# 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 ${⊢}{\phi }\to {A}={B}$
Assertion eqeq1d ${⊢}{\phi }\to \left({A}={C}↔{B}={C}\right)$

### Proof

Step Hyp Ref Expression
1 eqeq1d.1 ${⊢}{\phi }\to {A}={B}$
2 dfcleq ${⊢}{A}={B}↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}↔{x}\in {B}\right)$
3 2 biimpi ${⊢}{A}={B}\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}↔{x}\in {B}\right)$
4 bibi1 ${⊢}\left({x}\in {A}↔{x}\in {B}\right)\to \left(\left({x}\in {A}↔{x}\in {C}\right)↔\left({x}\in {B}↔{x}\in {C}\right)\right)$
5 4 alimi ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}↔{x}\in {B}\right)\to \forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\in {A}↔{x}\in {C}\right)↔\left({x}\in {B}↔{x}\in {C}\right)\right)$
6 albi ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\in {A}↔{x}\in {C}\right)↔\left({x}\in {B}↔{x}\in {C}\right)\right)\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}↔{x}\in {C}\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}↔{x}\in {C}\right)\right)$
7 1 3 5 6 4syl ${⊢}{\phi }\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}↔{x}\in {C}\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}↔{x}\in {C}\right)\right)$
8 dfcleq ${⊢}{A}={C}↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}↔{x}\in {C}\right)$
9 dfcleq ${⊢}{B}={C}↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}↔{x}\in {C}\right)$
10 7 8 9 3bitr4g ${⊢}{\phi }\to \left({A}={C}↔{B}={C}\right)$