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  4227  iinexgm  4292  xpiindim  4919  reldmm  5002  cnviinm  5332  iotam  5372  elfvm  5732  mptmex  5948  cbvriotavw  6052  uchoice  6375  suppssdc  6504  iinerm  6886  ixpiinm  7012  ixpsnf1o  7024  mapsnend  7105  mapsnen  7106  pw2f1odclem  7140  enumctlemm  7460  nnnninfeq  7474  exmidomni  7488  fodjum  7492  finacn  7566  exmidontriimlem4  7586  exmidontriim  7587  cc2  7639  suplocexprlemmu  8091  suplocsr  8182  axpre-suploc  8275  indfdc  9307  suprzubdc  10687  nninfdcex  10688  zsupssdc  10689  iseqf1olemqk  10964  seq3f1olemqsum  10970  reuccatpfxs1  11540  summodclem2  12173  summodc  12174  zsumdc  12175  fsum3  12178  isumz  12180  isumss  12182  fisumss  12183  isumss2  12184  fsum3cvg2  12185  fsumsersdc  12186  fsum3ser  12188  fsumsplit  12198  fsumsplitf  12199  isumlessdc  12287  prodfdivap  12338  cbvprod  12349  prodrbdclem  12362  prodmodclem2  12368  prodmodc  12369  zproddc  12370  fprodseq  12374  fprodntrivap  12375  prod1dc  12377  prodssdc  12380  fprodsplitdc  12387  fprod2dlemstep  12413  fproddivapf  12422  fprodsplitf  12423  nnmindc  12835  nnminle  12836  nninfctlemfo  12841  pcmptdvds  13152  nninfdclemp1  13398  ismnd  13790  sgrpidmndm  13791  dfgrp3me  13963  issubg2m  14050  gsumresfi  14262  subrgintm  14659  islssm  14802  islidlm  14924  neipsm  15397  dedekindeulemub  15861  dedekindeulemloc  15862  dedekindeulemlub  15863  suplociccex  15868  dedekindicclemub  15870  dedekindicclemloc  15871  dedekindicclemlub  15872  limcimo  15908  dvmptfsum  15968  elply2  15978  prmorcht  16299  lgsval  16345  lgsdir  16376  lgsdilem2  16377  lgsdi  16378  lgsne0  16379  lgsquadlem3  16420  lgsquad  16421  2sqlem8  16464  bj-charfunbi  17059  2alsraln0idm  17383