Metamath Proof Explorer

Theorem eleq2d

Description: Deduction from equality to equivalence of membership. (Contributed by NM, 27-Dec-1993) Reduce dependencies on axioms. (Revised by Wolf Lammen, 5-Dec-2019)

Ref Expression
Hypothesis eleq1d.1 ⊢ φ → A = B
Assertion eleq2d ⊢ φ → C ∈ A ↔ C ∈ B

Proof

Step Hyp Ref Expression
1 eleq1d.1 ⊢ φ → A = B
2 dfcleq ⊢ A = B ↔ ∀ x x ∈ A ↔ x ∈ B
3 1 2 sylib ⊢ φ → ∀ x x ∈ A ↔ x ∈ B
4 anbi2 ⊢ x ∈ A ↔ x ∈ B → x = C ∧ x ∈ A ↔ x = C ∧ x ∈ B
5 4 alexbii ⊢ ∀ x x ∈ A ↔ x ∈ B → ∃ x x = C ∧ x ∈ A ↔ ∃ x x = C ∧ x ∈ B
6 3 5 syl ⊢ φ → ∃ x x = C ∧ x ∈ A ↔ ∃ x x = C ∧ x ∈ B
7 dfclel ⊢ C ∈ A ↔ ∃ x x = C ∧ x ∈ A
8 dfclel ⊢ C ∈ B ↔ ∃ x x = C ∧ x ∈ B
9 6 7 8 3bitr4g ⊢ φ → C ∈ A ↔ C ∈ B