Metamath Proof Explorer

Theorem eqeq1dALT

Description: Alternate proof of eqeq1d , shorter but requiring ax-12 . (Contributed by NM, 27-Dec-1993) (Revised by Wolf Lammen, 19-Nov-2019) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis eqeq1d.1 ⊢ φ → A = B
Assertion eqeq1dALT ⊢ φ → A = C ↔ B = C

Proof

Step Hyp Ref Expression
1 eqeq1d.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 bibi1d ⊢ φ → x ∈ A ↔ x ∈ C ↔ x ∈ B ↔ x ∈ C
6 5 albidv ⊢ φ → ∀ x x ∈ A ↔ x ∈ C ↔ ∀ x x ∈ B ↔ x ∈ C
7 dfcleq ⊢ A = C ↔ ∀ x x ∈ A ↔ x ∈ C
8 dfcleq ⊢ B = C ↔ ∀ x x ∈ B ↔ x ∈ C
9 6 7 8 3bitr4g ⊢ φ → A = C ↔ B = C