Metamath Proof Explorer

Theorem disjeq2

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

Ref Expression
Assertion disjeq2 ⊢∀x∈AB=C→Disjx∈AB↔Disjx∈AC

Proof

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