# Metamath Proof Explorer

## Theorem eleq1w

Description: Weaker version of eleq1 (but more general than elequ1 ) not depending on ax-ext nor df-cleq .

Note that this provides a proof of ax-8 from Tarski's FOL and dfclel (simply consider an instance where A is replaced by a setvar and deduce the forward implication by biimpd ), which shows that dfclel is too powerful to be used as a definition instead of df-clel . (Contributed by BJ, 24-Jun-2019)

Ref Expression
Assertion eleq1w ${⊢}{x}={y}\to \left({x}\in {A}↔{y}\in {A}\right)$

### Proof

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