This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem parteq2

Description: Equality theorem for partition. (Contributed by Peter Mazsa, 25-Jul-2024)

Ref Expression
Assertion parteq2 ⊢ A = B → R Part A ↔ R Part B

Proof

Step Hyp Ref Expression
1 eqeq2 ⊢ A = B → dom ⁡ R / R = A ↔ dom ⁡ R / R = B
2 1 anbi2d ⊢ A = B → Disj R ∧ dom ⁡ R / R = A ↔ Disj R ∧ dom ⁡ R / R = B
3 dfpart2 ⊢ R Part A ↔ Disj R ∧ dom ⁡ R / R = A
4 dfpart2 ⊢ R Part B ↔ Disj R ∧ dom ⁡ R / R = B
5 2 3 4 3bitr4g ⊢ A = B → R Part A ↔ R Part B