Theorem eleq1w 2215

Description: Weaker version of eleq1 2217 (but more general than elequ1 2129) not depending on ax-ext 2136 nor df-cleq 2147. (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 1802	. 2 |- ( x = y -> ( E. z ( z = x /\ z e. A ) <-> E. z ( z = y /\ z e. A ) ) )
4		df-clel 2150	. 2 |- ( x e. A <-> E. z ( z = x /\ z e. A ) )
5		df-clel 2150	. 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 2125

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 1481  ax-4 1487  ax-17 1503  ax-i9 1507  ax-ial 1511

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

This theorem is referenced by:  clelsb3f  2300  cbvralvw  2681  cbvrexvw  2682  cbvreuvw  2683  dfdif3  3213  dfss4st  3336  abn0m  3415  r19.2m  3476  cbvmptf  4054  iinexgm  4111  xpiindim  4716  cnviinm  5120  iinerm  6541  ixpiinm  6658  ixpsnf1o  6670  mapsnen  6745  enumctlemm  7044  exmidomni  7064  fodjum  7068  exmidontriimlem4  7138  exmidontriim  7139  cc2  7166  suplocexprlemmu  7617  suplocsr  7708  axpre-suploc  7801  iseqf1olemqk  10371  seq3f1olemqsum  10377  summodclem2  11256  summodc  11257  zsumdc  11258  fsum3  11261  isumz  11263  isumss  11265  fisumss  11266  isumss2  11267  fsum3cvg2  11268  fsumsersdc  11269  fsum3ser  11271  fsumsplit  11281  fsumsplitf  11282  isumlessdc  11370  prodfdivap  11421  cbvprod  11432  prodrbdclem  11445  prodmodclem2  11451  prodmodc  11452  zproddc  11453  fprodseq  11457  fprodntrivap  11458  prod1dc  11460  prodssdc  11463  fprodsplitdc  11470  fprod2dlemstep  11496  fproddivapf  11505  fprodsplitf  11506  neipsm  12493  dedekindeulemub  12935  dedekindeulemloc  12936  dedekindeulemlub  12937  suplociccex  12942  dedekindicclemub  12944  dedekindicclemloc  12945  dedekindicclemlub  12946  limcimo  12973  bj-charfunbi  13324  nninfalllemn  13520