Theorem eleq2w

Description: Weaker version of eleq2 (but more general than elequ2 ) not depending on ax-ext nor df-cleq . (Contributed by BJ, 29-Sep-2019)

	Ref	Expression
Assertion	eleq2w	|- ( x = y -> ( A e. x <-> A e. y ) )

Proof

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