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  9298  suprzubdc  10671  nninfdcex  10672  zsupssdc  10673  iseqf1olemqk  10944  seq3f1olemqsum  10950  reuccatpfxs1  11519  summodclem2  12149  summodc  12150  zsumdc  12151  fsum3  12154  isumz  12156  isumss  12158  fisumss  12159  isumss2  12160  fsum3cvg2  12161  fsumsersdc  12162  fsum3ser  12164  fsumsplit  12174  fsumsplitf  12175  isumlessdc  12263  prodfdivap  12314  cbvprod  12325  prodrbdclem  12338  prodmodclem2  12344  prodmodc  12345  zproddc  12346  fprodseq  12350  fprodntrivap  12351  prod1dc  12353  prodssdc  12356  fprodsplitdc  12363  fprod2dlemstep  12389  fproddivapf  12398  fprodsplitf  12399  nnmindc  12811  nnminle  12812  nninfctlemfo  12817  pcmptdvds  13124  nninfdclemp1  13341  ismnd  13732  sgrpidmndm  13733  dfgrp3me  13905  issubg2m  13992  subrgintm  14551  islssm  14694  islidlm  14816  neipsm  15255  dedekindeulemub  15719  dedekindeulemloc  15720  dedekindeulemlub  15721  suplociccex  15726  dedekindicclemub  15728  dedekindicclemloc  15729  dedekindicclemlub  15730  limcimo  15766  dvmptfsum  15826  elply2  15836  lgsval  16123  lgsdir  16154  lgsdilem2  16155  lgsdi  16156  lgsne0  16157  lgsquadlem3  16198  lgsquad  16199  2sqlem8  16242  bj-charfunbi  16837  2alsraln0idm  17159