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

Metamath Proof Explorer

Theorem disjeq1

Description: Equality theorem for disjoint collection. (Contributed by Mario Carneiro, 14-Nov-2016)

Ref Expression
Assertion disjeq1 ⊢ A = B → Disj x ∈ A C ↔ Disj x ∈ B C

Proof

Step Hyp Ref Expression
1 eqimss2 ⊢ A = B → B ⊆ A
2 disjss1 ⊢ B ⊆ A → Disj x ∈ A C → Disj x ∈ B C
3 1 2 syl ⊢ A = B → Disj x ∈ A C → Disj x ∈ B C
4 eqimss ⊢ A = B → A ⊆ B
5 disjss1 ⊢ A ⊆ B → Disj x ∈ B C → Disj x ∈ A C
6 4 5 syl ⊢ A = B → Disj x ∈ B C → Disj x ∈ A C
7 3 6 impbid ⊢ A = B → Disj x ∈ A C ↔ Disj x ∈ B C