Theorem eleq1w 2266

Description: Weaker version of eleq1 2268 (but more general than elequ1 2180) not depending on ax-ext 2187 nor df-cleq 2198. (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 1736	. . . 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 1848	. 2 |- ( x = y -> ( E. z ( z = x /\ z e. A ) <-> E. z ( z = y /\ z e. A ) ) )
4		df-clel 2201	. 2 |- ( x e. A <-> E. z ( z = x /\ z e. A ) )
5		df-clel 2201	. 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 1515   e. wcel 2176

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557

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

This theorem is referenced by:  clelsb1f  2352  cbvralfw  2728  cbvrexfw  2729  cbvralvw  2742  cbvrexvw  2743  cbvreuvw  2744  dfdif3  3283  dfss4st  3406  abn0m  3486  r19.2m  3547  cbvmptf  4139  iinexgm  4199  xpiindim  4816  cnviinm  5225  iotam  5264  elfvm  5611  uchoice  6225  iinerm  6696  ixpiinm  6813  ixpsnf1o  6825  mapsnen  6905  pw2f1odclem  6933  enumctlemm  7218  nnnninfeq  7232  exmidomni  7246  fodjum  7250  finacn  7318  exmidontriimlem4  7338  exmidontriim  7339  cc2  7381  suplocexprlemmu  7833  suplocsr  7924  axpre-suploc  8017  suprzubdc  10381  nninfdcex  10382  zsupssdc  10383  iseqf1olemqk  10654  seq3f1olemqsum  10660  summodclem2  11726  summodc  11727  zsumdc  11728  fsum3  11731  isumz  11733  isumss  11735  fisumss  11736  isumss2  11737  fsum3cvg2  11738  fsumsersdc  11739  fsum3ser  11741  fsumsplit  11751  fsumsplitf  11752  isumlessdc  11840  prodfdivap  11891  cbvprod  11902  prodrbdclem  11915  prodmodclem2  11921  prodmodc  11922  zproddc  11923  fprodseq  11927  fprodntrivap  11928  prod1dc  11930  prodssdc  11933  fprodsplitdc  11940  fprod2dlemstep  11966  fproddivapf  11975  fprodsplitf  11976  nnmindc  12388  nnminle  12389  nninfctlemfo  12394  pcmptdvds  12701  nninfdclemp1  12854  ismnd  13284  sgrpidmndm  13285  dfgrp3me  13465  issubg2m  13558  subrgintm  14038  islssm  14152  islidlm  14274  neipsm  14659  dedekindeulemub  15123  dedekindeulemloc  15124  dedekindeulemlub  15125  suplociccex  15130  dedekindicclemub  15132  dedekindicclemloc  15133  dedekindicclemlub  15134  limcimo  15170  dvmptfsum  15230  elply2  15240  lgsval  15514  lgsdir  15545  lgsdilem2  15546  lgsdi  15547  lgsne0  15548  lgsquadlem3  15589  lgsquad  15590  2sqlem8  15633  bj-charfunbi  15784