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

Metamath Proof Explorer

Theorem disjeq2dv

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

Ref Expression
Hypothesis disjeq2dv.1 ⊢ φ ∧ x ∈ A → B = C
Assertion disjeq2dv ⊢ φ → Disj x ∈ A B ↔ Disj x ∈ A C

Proof

Step Hyp Ref Expression
1 disjeq2dv.1 ⊢ φ ∧ x ∈ A → B = C
2 1 ralrimiva ⊢ φ → ∀ x ∈ A B = C
3 disjeq2 ⊢ ∀ x ∈ A B = C → Disj x ∈ A B ↔ Disj x ∈ A C
4 2 3 syl ⊢ φ → Disj x ∈ A B ↔ Disj x ∈ A C