Theorem eleq1w 2201

Description: Weaker version of eleq1 2203 (but more general than elequ1 1691) not depending on ax-ext 2122 nor df-cleq 2133. (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 1690	. . . 4 |- ( x = y -> ( z = x <-> z = y ) )
2	1	anbi1d 461	. . 3 |- ( x = y -> ( ( z = x /\ z e. A ) <-> ( z = y /\ z e. A ) ) )
3	2	exbidv 1798	. 2 |- ( x = y -> ( E. z ( z = x /\ z e. A ) <-> E. z ( z = y /\ z e. A ) ) )
4		df-clel 2136	. 2 |- ( x e. A <-> E. z ( z = x /\ z e. A ) )
5		df-clel 2136	. 2 |- ( y e. A <-> E. z ( z = y /\ z e. A ) )
6	3, 4, 5	3bitr4g 222	1 |- ( x = y -> ( x e. A <-> y e. A ) )

Syntax hints:   -> wi 4   /\ wa 103   <-> wb 104   E.wex 1469   e. wcel 1481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515

This theorem depends on definitions:  df-bi 116  df-clel 2136

This theorem is referenced by:  clelsb3f  2286  dfdif3  3191  dfss4st  3314  abn0m  3393  r19.2m  3454  cbvmptf  4030  iinexgm  4087  xpiindim  4684  cnviinm  5088  iinerm  6509  ixpiinm  6626  ixpsnf1o  6638  mapsnen  6713  enumctlemm  7007  exmidomni  7022  fodjum  7026  cc2  7099  suplocexprlemmu  7550  suplocsr  7641  axpre-suploc  7734  iseqf1olemqk  10298  seq3f1olemqsum  10304  summodclem2  11183  summodc  11184  zsumdc  11185  fsum3  11188  isumz  11190  isumss  11192  fisumss  11193  isumss2  11194  fsum3cvg2  11195  fsumsersdc  11196  fsum3ser  11198  fsumsplit  11208  fsumsplitf  11209  isumlessdc  11297  prodfdivap  11348  cbvprod  11359  prodrbdclem  11372  prodmodclem2  11378  prodmodc  11379  zproddc  11380  fprodseq  11384  neipsm  12362  dedekindeulemub  12804  dedekindeulemloc  12805  dedekindeulemlub  12806  suplociccex  12811  dedekindicclemub  12813  dedekindicclemloc  12814  dedekindicclemlub  12815  limcimo  12842  nninfalllemn  13377