# Metamath Proof Explorer

## Theorem eleq1d

Description: Deduction from equality to equivalence of membership. (Contributed by NM, 21-Jun-1993) Allow shortening of eleq1 . (Revised by Wolf Lammen, 20-Nov-2019)

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

### Proof

Step Hyp Ref Expression
1 eleq1d.1 ${⊢}{\phi }\to {A}={B}$
2 1 eqeq2d ${⊢}{\phi }\to \left({x}={A}↔{x}={B}\right)$
3 2 anbi1d ${⊢}{\phi }\to \left(\left({x}={A}\wedge {x}\in {C}\right)↔\left({x}={B}\wedge {x}\in {C}\right)\right)$
4 3 exbidv ${⊢}{\phi }\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}={A}\wedge {x}\in {C}\right)↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}={B}\wedge {x}\in {C}\right)\right)$
5 dfclel ${⊢}{A}\in {C}↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}={A}\wedge {x}\in {C}\right)$
6 dfclel ${⊢}{B}\in {C}↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}={B}\wedge {x}\in {C}\right)$
7 4 5 6 3bitr4g ${⊢}{\phi }\to \left({A}\in {C}↔{B}\in {C}\right)$