Theorem eleq1w 2268

Description: Weaker version of eleq1 2270 (but more general than elequ1 2182) not depending on ax-ext 2189 nor df-cleq 2200. (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 1737	. . . 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 1849	. 2 |- ( x = y -> ( E. z ( z = x /\ z e. A ) <-> E. z ( z = y /\ z e. A ) ) )
4		df-clel 2203	. 2 |- ( x e. A <-> E. z ( z = x /\ z e. A ) )
5		df-clel 2203	. 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 1516   e. wcel 2178

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558

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

This theorem is referenced by:  clelsb1f  2354  cbvrmow  2691  cbvralfw  2731  cbvrexfw  2732  cbvralvw  2746  cbvrexvw  2747  cbvreuvw  2748  dfdif3  3291  dfss4st  3414  abn0m  3494  r19.2m  3555  cbvmptf  4154  iinexgm  4214  xpiindim  4833  cnviinm  5243  iotam  5282  elfvm  5632  uchoice  6246  iinerm  6717  ixpiinm  6834  ixpsnf1o  6846  mapsnen  6927  pw2f1odclem  6956  enumctlemm  7242  nnnninfeq  7256  exmidomni  7270  fodjum  7274  finacn  7347  exmidontriimlem4  7367  exmidontriim  7368  cc2  7414  suplocexprlemmu  7866  suplocsr  7957  axpre-suploc  8050  suprzubdc  10416  nninfdcex  10417  zsupssdc  10418  iseqf1olemqk  10689  seq3f1olemqsum  10695  reuccatpfxs1  11238  summodclem2  11808  summodc  11809  zsumdc  11810  fsum3  11813  isumz  11815  isumss  11817  fisumss  11818  isumss2  11819  fsum3cvg2  11820  fsumsersdc  11821  fsum3ser  11823  fsumsplit  11833  fsumsplitf  11834  isumlessdc  11922  prodfdivap  11973  cbvprod  11984  prodrbdclem  11997  prodmodclem2  12003  prodmodc  12004  zproddc  12005  fprodseq  12009  fprodntrivap  12010  prod1dc  12012  prodssdc  12015  fprodsplitdc  12022  fprod2dlemstep  12048  fproddivapf  12057  fprodsplitf  12058  nnmindc  12470  nnminle  12471  nninfctlemfo  12476  pcmptdvds  12783  nninfdclemp1  12936  ismnd  13366  sgrpidmndm  13367  dfgrp3me  13547  issubg2m  13640  subrgintm  14120  islssm  14234  islidlm  14356  neipsm  14741  dedekindeulemub  15205  dedekindeulemloc  15206  dedekindeulemlub  15207  suplociccex  15212  dedekindicclemub  15214  dedekindicclemloc  15215  dedekindicclemlub  15216  limcimo  15252  dvmptfsum  15312  elply2  15322  lgsval  15596  lgsdir  15627  lgsdilem2  15628  lgsdi  15629  lgsne0  15630  lgsquadlem3  15671  lgsquad  15672  2sqlem8  15715  bj-charfunbi  15946