Metamath Proof Explorer

Theorem eleq2dALT

Description: Alternate proof of eleq2d , shorter at the expense of requiring ax-12 . (Contributed by NM, 27-Dec-1993) (Revised by Wolf Lammen, 20-Nov-2019) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis eleq1d.1 ⊢ φ → A = B
Assertion eleq2dALT ⊢ φ → 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 3 19.21bi ⊢ φ → x ∈ A ↔ x ∈ B
5 4 anbi2d ⊢ φ → x = C ∧ x ∈ A ↔ x = C ∧ x ∈ B
6 5 exbidv ⊢ φ → ∃ 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