Metamath Proof Explorer

Theorem parteq1

Description: Equality theorem for partition. (Contributed by Peter Mazsa, 5-Oct-2021)

Ref Expression
Assertion parteq1 
|- ( R = S -> ( R Part A <-> S Part A ) )

Proof

Step Hyp Ref Expression
1 disjdmqseqeq1 
 |-  ( R = S -> ( ( Disj R /\ ( dom R /. R ) = A ) <-> ( Disj S /\ ( dom S /. S ) = A ) ) )
2 dfpart2 
 |-  ( R Part A <-> ( Disj R /\ ( dom R /. R ) = A ) )
3 dfpart2 
 |-  ( S Part A <-> ( Disj S /\ ( dom S /. S ) = A ) )
4 1 2 3 3bitr4g 
 |-  ( R = S -> ( R Part A <-> S Part A ) )