Metamath Proof Explorer

Theorem eqeq1d

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

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

Proof

Step Hyp Ref Expression
1 eqeq1d.1 ⊢ φ → A = B
2 dfcleq ⊢ A = B ↔ ∀ x x ∈ A ↔ x ∈ B
3 2 biimpi ⊢ A = B → ∀ x x ∈ A ↔ x ∈ B
4 bibi1 ⊢ x ∈ A ↔ x ∈ B → x ∈ A ↔ x ∈ C ↔ x ∈ B ↔ x ∈ C
5 4 alimi ⊢ ∀ x x ∈ A ↔ x ∈ B → ∀ x x ∈ A ↔ x ∈ C ↔ x ∈ B ↔ x ∈ C
6 albi ⊢ ∀ x x ∈ A ↔ x ∈ C ↔ x ∈ B ↔ x ∈ C → ∀ x x ∈ A ↔ x ∈ C ↔ ∀ x x ∈ B ↔ x ∈ C
7 1 3 5 6 4syl ⊢ φ → ∀ x x ∈ A ↔ x ∈ C ↔ ∀ x x ∈ B ↔ x ∈ C
8 dfcleq ⊢ A = C ↔ ∀ x x ∈ A ↔ x ∈ C
9 dfcleq ⊢ B = C ↔ ∀ x x ∈ B ↔ x ∈ C
10 7 8 9 3bitr4g ⊢ φ → A = C ↔ B = C