This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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