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