Theorem eleq1w 2295

Description: Weaker version of eleq1 2297 (but more general than elequ1 2209) not depending on ax-ext 2216 nor df-cleq 2227. (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 1761	. . . 4 |- ( x = y -> ( z = x <-> z = y ) )
2	1	anbi1d 465	. . 3 |- ( x = y -> ( ( z = x /\ z e. A ) <-> ( z = y /\ z e. A ) ) )
3	2	exbidv 1874	. 2 |- ( x = y -> ( E. z ( z = x /\ z e. A ) <-> E. z ( z = y /\ z e. A ) ) )
4		df-clel 2230	. 2 |- ( x e. A <-> E. z ( z = x /\ z e. A ) )
5		df-clel 2230	. 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 ) )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   E.wex 1541   e. wcel 2205

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583

This theorem depends on definitions:  df-bi 117  df-clel 2230

This theorem is referenced by:  clelsb1f  2390  cbvrmow  2729  cbvralfw  2769  cbvrexfw  2770  cbvralvw  2784  cbvrexvw  2785  cbvreuvw  2786  dfdif3  3333  dfss4st  3458  abn0m  3538  r19.2m  3601  rabsnifsb  3763  cbvmptf  4210  iinexgm  4272  xpiindim  4899  reldmm  4982  cnviinm  5311  iotam  5351  elfvm  5710  cbvriotavw  6024  uchoice  6346  suppssdc  6475  iinerm  6856  ixpiinm  6974  ixpsnf1o  6986  mapsnend  7067  mapsnen  7068  pw2f1odclem  7102  enumctlemm  7420  nnnninfeq  7434  exmidomni  7448  fodjum  7452  finacn  7526  exmidontriimlem4  7546  exmidontriim  7547  cc2  7599  suplocexprlemmu  8051  suplocsr  8142  axpre-suploc  8235  suprzubdc  10625  nninfdcex  10626  zsupssdc  10627  iseqf1olemqk  10898  seq3f1olemqsum  10904  reuccatpfxs1  11469  summodclem2  12099  summodc  12100  zsumdc  12101  fsum3  12104  isumz  12106  isumss  12108  fisumss  12109  isumss2  12110  fsum3cvg2  12111  fsumsersdc  12112  fsum3ser  12114  fsumsplit  12124  fsumsplitf  12125  isumlessdc  12213  prodfdivap  12264  cbvprod  12275  prodrbdclem  12288  prodmodclem2  12294  prodmodc  12295  zproddc  12296  fprodseq  12300  fprodntrivap  12301  prod1dc  12303  prodssdc  12306  fprodsplitdc  12313  fprod2dlemstep  12339  fproddivapf  12348  fprodsplitf  12349  nnmindc  12761  nnminle  12762  nninfctlemfo  12767  pcmptdvds  13074  nninfdclemp1  13291  ismnd  13686  sgrpidmndm  13687  dfgrp3me  13861  issubg2m  13948  subrgintm  14495  islssm  14637  islidlm  14759  neipsm  15151  dedekindeulemub  15615  dedekindeulemloc  15616  dedekindeulemlub  15617  suplociccex  15622  dedekindicclemub  15624  dedekindicclemloc  15625  dedekindicclemlub  15626  limcimo  15662  dvmptfsum  15722  elply2  15732  lgsval  16009  lgsdir  16040  lgsdilem2  16041  lgsdi  16042  lgsne0  16043  lgsquadlem3  16084  lgsquad  16085  2sqlem8  16128  bj-charfunbi  16723