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↔∀xx∈A↔x∈B
3 2 biimpi ⊢A=B→∀xx∈A↔x∈B
4 bibi1 ⊢x∈A↔x∈B→x∈A↔x∈C↔x∈B↔x∈C
5 4 alimi ⊢∀xx∈A↔x∈B→∀xx∈A↔x∈C↔x∈B↔x∈C
6 albi ⊢∀xx∈A↔x∈C↔x∈B↔x∈C→∀xx∈A↔x∈C↔∀xx∈B↔x∈C
7 1 3 5 6 4syl ⊢φ→∀xx∈A↔x∈C↔∀xx∈B↔x∈C
8 dfcleq ⊢A=C↔∀xx∈A↔x∈C
9 dfcleq ⊢B=C↔∀xx∈B↔x∈C
10 7 8 9 3bitr4g ⊢φ→A=C↔B=C