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