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 -> ( x e. A <-> y e. A ) )

Proof

Step	Hyp	Ref	Expression
1		equequ2	|- ( x = y -> ( z = x <-> z = y ) )
2	1	anbi1d	|- ( x = y -> ( ( z = x /\ z e. A ) <-> ( z = y /\ z e. A ) ) )
3	2	exbidv	|- ( x = y -> ( E. z ( z = x /\ z e. A ) <-> E. z ( z = y /\ z e. A ) ) )
4		dfclel	|- ( x e. A <-> E. z ( z = x /\ z e. A ) )
5		dfclel	|- ( y e. A <-> E. z ( z = y /\ z e. A ) )
6	3 4 5	3bitr4g	|- ( x = y -> ( x e. A <-> y e. A ) )