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 ) )