Theorem eleq1w 2148

Description: Weaker version of eleq1 2150 (but more general than elequ1 1647) not depending on ax-ext 2070 nor df-cleq 2081. (Contributed by BJ, 24-Jun-2019.)

Assertion

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

Proof of Theorem eleq1w

Dummy variable z is distinct from all other variables.

Step	Hyp	Ref	Expression
1		equequ2 1646	. . . 4 |- ( x = y -> ( z = x <-> z = y ) )
2	1	anbi1d 453	. . 3 |- ( x = y -> ( ( z = x /\ z e. A ) <-> ( z = y /\ z e. A ) ) )
3	2	exbidv 1753	. 2 |- ( x = y -> ( E. z ( z = x /\ z e. A ) <-> E. z ( z = y /\ z e. A ) ) )
4		df-clel 2084	. 2 |- ( x e. A <-> E. z ( z = x /\ z e. A ) )
5		df-clel 2084	. 2 |- ( y e. A <-> E. z ( z = y /\ z e. A ) )
6	3, 4, 5	3bitr4g 221	1 |- ( x = y -> ( x e. A <-> y e. A ) )

Syntax hints:   -> wi 4   /\ wa 102   <-> wb 103   E.wex 1426   e. wcel 1438

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472

This theorem depends on definitions:  df-bi 115  df-clel 2084

This theorem is referenced by:  clelsb3f  2232  dfdif3  3110  dfss4st  3232  abn0m  3308  cbvmptf  3932  mapsnen  6526  exmidomni  6796  fodjuomnilemm  6799  iseqf1olemqk  9919  seq3f1olemqsum  9925  isummolem2  10768  isummo  10769  zisum  10770  fisum  10774  isumz  10777  isumss  10779  fisumss  10780  isumss2  10781  fisumcvg2  10782  fsum3cvg2  10783  fisumsers  10784  fisumser  10786  fsumsplit  10797  fsumsplitf  10798  isumlessdc  10886  nninfalllemn  11853