Metamath Proof Explorer

Theorem disjdmqseqeq1

Description: Lemma for the equality theorem for partition parteq1 . (Contributed by Peter Mazsa, 5-Oct-2021)

Ref Expression
Assertion disjdmqseqeq1 
|- ( R = S -> ( ( Disj R /\ ( dom R /. R ) = A ) <-> ( Disj S /\ ( dom S /. S ) = A ) ) )

Proof

Step Hyp Ref Expression
1 disjeq 
 |-  ( R = S -> ( Disj R <-> Disj S ) )
2 dmqseqeq1 
 |-  ( R = S -> ( ( dom R /. R ) = A <-> ( dom S /. S ) = A ) )
3 1 2 anbi12d 
 |-  ( R = S -> ( ( Disj R /\ ( dom R /. R ) = A ) <-> ( Disj S /\ ( dom S /. S ) = A ) ) )