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 ) )

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

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 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 theorem depends on definitions:  df-bi 117  df-clel 2234

This theorem is referenced by:  clelsb1f  2396  cbvrmow  2735  cbvralfw  2775  cbvrexfw  2776  cbvralvw  2790  cbvrexvw  2791  cbvreuvw  2792  dfdif3  3339  dfss4st  3464  abn0m  3547  r19.2m  3611  rabsnifsb  3773  cbvmptf  4220  iinexgm  4285  xpiindim  4912  reldmm  4995  cnviinm  5324  iotam  5364  elfvm  5723  cbvriotavw  6039  uchoice  6361  suppssdc  6490  iinerm  6871  ixpiinm  6996  ixpsnf1o  7008  mapsnend  7089  mapsnen  7090  pw2f1odclem  7124  enumctlemm  7444  nnnninfeq  7458  exmidomni  7472  fodjum  7476  finacn  7550  exmidontriimlem4  7570  exmidontriim  7571  cc2  7623  suplocexprlemmu  8075  suplocsr  8166  axpre-suploc  8259  suprzubdc  10649  nninfdcex  10650  zsupssdc  10651  iseqf1olemqk  10922  seq3f1olemqsum  10928  reuccatpfxs1  11497  summodclem2  12127  summodc  12128  zsumdc  12129  fsum3  12132  isumz  12134  isumss  12136  fisumss  12137  isumss2  12138  fsum3cvg2  12139  fsumsersdc  12140  fsum3ser  12142  fsumsplit  12152  fsumsplitf  12153  isumlessdc  12241  prodfdivap  12292  cbvprod  12303  prodrbdclem  12316  prodmodclem2  12322  prodmodc  12323  zproddc  12324  fprodseq  12328  fprodntrivap  12329  prod1dc  12331  prodssdc  12334  fprodsplitdc  12341  fprod2dlemstep  12367  fproddivapf  12376  fprodsplitf  12377  nnmindc  12789  nnminle  12790  nninfctlemfo  12795  pcmptdvds  13102  nninfdclemp1  13319  ismnd  13709  sgrpidmndm  13710  dfgrp3me  13882  issubg2m  13969  subrgintm  14524  islssm  14666  islidlm  14788  neipsm  15178  dedekindeulemub  15642  dedekindeulemloc  15643  dedekindeulemlub  15644  suplociccex  15649  dedekindicclemub  15651  dedekindicclemloc  15652  dedekindicclemlub  15653  limcimo  15689  dvmptfsum  15749  elply2  15759  lgsval  16037  lgsdir  16068  lgsdilem2  16069  lgsdi  16070  lgsne0  16071  lgsquadlem3  16112  lgsquad  16113  2sqlem8  16156  bj-charfunbi  16751