Theorem eleq1w 2299

Description: Weaker version of eleq1 2301 (but more general than elequ1 2213) not depending on ax-ext 2220 nor df-cleq 2231. (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 1765	. . . 4 |- ( x = y -> ( z = x <-> z = y ) )
2	1	anbi1d 469	. . 3 |- ( x = y -> ( ( z = x /\ z e. A ) <-> ( z = y /\ z e. A ) ) )
3	2	exbidv 1878	. 2 |- ( x = y -> ( E. z ( z = x /\ z e. A ) <-> E. z ( z = y /\ z e. A ) ) )
4		df-clel 2234	. 2 |- ( x e. A <-> E. z ( z = x /\ z e. A ) )
5		df-clel 2234	. 2 |- ( y e. A <-> E. z ( z = y /\ z e. A ) )
6	3, 4, 5	3bitr4g 223	1 |- ( x = y -> ( x e. A <-> y e. A ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   <-> wb 105   E.wex 1545   e. wcel 2209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587

This proof depends on definitions:  df-bi 117  df-clel 2234

This theorem is used by:  clelsb1f  2396  cbvrmow  2735  cbvralfw  2775  cbvrexfw  2776  cbvralvw  2790  cbvrexvw  2791  cbvreuvw  2792  dfdif3  3339  dfss4st  3464  abn0m  3547  r19.2m  3614  rabsnifsb  3777  cbvmptf  4225  iinexgm  4290  xpiindim  4917  reldmm  5000  cnviinm  5329  iotam  5369  elfvm  5729  mptmex  5945  cbvriotavw  6049  uchoice  6371  suppssdc  6500  iinerm  6881  ixpiinm  7006  ixpsnf1o  7018  mapsnend  7099  mapsnen  7100  pw2f1odclem  7134  enumctlemm  7454  nnnninfeq  7468  exmidomni  7482  fodjum  7486  finacn  7560  exmidontriimlem4  7580  exmidontriim  7581  cc2  7633  suplocexprlemmu  8085  suplocsr  8176  axpre-suploc  8269  indfdc  9300  suprzubdc  10681  nninfdcex  10682  zsupssdc  10683  iseqf1olemqk  10957  seq3f1olemqsum  10963  reuccatpfxs1  11533  summodclem2  12165  summodc  12166  zsumdc  12167  fsum3  12170  isumz  12172  isumss  12174  fisumss  12175  isumss2  12176  fsum3cvg2  12177  fsumsersdc  12178  fsum3ser  12180  fsumsplit  12190  fsumsplitf  12191  isumlessdc  12279  prodfdivap  12330  cbvprod  12341  prodrbdclem  12354  prodmodclem2  12360  prodmodc  12361  zproddc  12362  fprodseq  12366  fprodntrivap  12367  prod1dc  12369  prodssdc  12372  fprodsplitdc  12379  fprod2dlemstep  12405  fproddivapf  12414  fprodsplitf  12415  nnmindc  12827  nnminle  12828  nninfctlemfo  12833  pcmptdvds  13144  nninfdclemp1  13390  ismnd  13781  sgrpidmndm  13782  dfgrp3me  13954  issubg2m  14041  subrgintm  14600  islssm  14743  islidlm  14865  neipsm  15304  dedekindeulemub  15768  dedekindeulemloc  15769  dedekindeulemlub  15770  suplociccex  15775  dedekindicclemub  15777  dedekindicclemloc  15778  dedekindicclemlub  15779  limcimo  15815  dvmptfsum  15875  elply2  15885  lgsval  16221  lgsdir  16252  lgsdilem2  16253  lgsdi  16254  lgsne0  16255  lgsquadlem3  16296  lgsquad  16297  2sqlem8  16340  bj-charfunbi  16935  2alsraln0idm  17257