Metamath Proof Explorer

Theorem disjeq2

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

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

Proof

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