# Metamath Proof Explorer

## Theorem eleq2d

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

Ref Expression
Hypothesis eleq1d.1 ${⊢}{\phi }\to {A}={B}$
Assertion eleq2d ${⊢}{\phi }\to \left({C}\in {A}↔{C}\in {B}\right)$

### Proof

Step Hyp Ref Expression
1 eleq1d.1 ${⊢}{\phi }\to {A}={B}$
2 dfcleq ${⊢}{A}={B}↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}↔{x}\in {B}\right)$
3 1 2 sylib ${⊢}{\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}↔{x}\in {B}\right)$
4 anbi2 ${⊢}\left({x}\in {A}↔{x}\in {B}\right)\to \left(\left({x}={C}\wedge {x}\in {A}\right)↔\left({x}={C}\wedge {x}\in {B}\right)\right)$
5 4 alexbii ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}↔{x}\in {B}\right)\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}={C}\wedge {x}\in {A}\right)↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}={C}\wedge {x}\in {B}\right)\right)$
6 3 5 syl ${⊢}{\phi }\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}={C}\wedge {x}\in {A}\right)↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}={C}\wedge {x}\in {B}\right)\right)$
7 dfclel ${⊢}{C}\in {A}↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}={C}\wedge {x}\in {A}\right)$
8 dfclel ${⊢}{C}\in {B}↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}={C}\wedge {x}\in {B}\right)$
9 6 7 8 3bitr4g ${⊢}{\phi }\to \left({C}\in {A}↔{C}\in {B}\right)$