Theorem eleq1w 2292

Description: Weaker version of eleq1 2294 (but more general than elequ1 2206) not depending on ax-ext 2213 nor df-cleq 2224. (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 1761	. . . 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 1873	. 2 |- ( x = y -> ( E. z ( z = x /\ z e. A ) <-> E. z ( z = y /\ z e. A ) ) )
4		df-clel 2227	. 2 |- ( x e. A <-> E. z ( z = x /\ z e. A ) )
5		df-clel 2227	. 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 1541   e. wcel 2202

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583

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

This theorem is referenced by:  clelsb1f  2379  cbvrmow  2717  cbvralfw  2757  cbvrexfw  2758  cbvralvw  2772  cbvrexvw  2773  cbvreuvw  2774  dfdif3  3319  dfss4st  3442  abn0m  3522  r19.2m  3583  rabsnifsb  3741  cbvmptf  4188  iinexgm  4249  xpiindim  4873  reldmm  4956  cnviinm  5285  iotam  5325  elfvm  5681  cbvriotavw  5992  uchoice  6309  suppssdc  6438  iinerm  6819  ixpiinm  6936  ixpsnf1o  6948  mapsnen  7029  pw2f1odclem  7063  enumctlemm  7373  nnnninfeq  7387  exmidomni  7401  fodjum  7405  finacn  7479  exmidontriimlem4  7499  exmidontriim  7500  cc2  7546  suplocexprlemmu  7998  suplocsr  8089  axpre-suploc  8182  suprzubdc  10559  nninfdcex  10560  zsupssdc  10561  iseqf1olemqk  10832  seq3f1olemqsum  10838  reuccatpfxs1  11394  summodclem2  12023  summodc  12024  zsumdc  12025  fsum3  12028  isumz  12030  isumss  12032  fisumss  12033  isumss2  12034  fsum3cvg2  12035  fsumsersdc  12036  fsum3ser  12038  fsumsplit  12048  fsumsplitf  12049  isumlessdc  12137  prodfdivap  12188  cbvprod  12199  prodrbdclem  12212  prodmodclem2  12218  prodmodc  12219  zproddc  12220  fprodseq  12224  fprodntrivap  12225  prod1dc  12227  prodssdc  12230  fprodsplitdc  12237  fprod2dlemstep  12263  fproddivapf  12272  fprodsplitf  12273  nnmindc  12685  nnminle  12686  nninfctlemfo  12691  pcmptdvds  12998  nninfdclemp1  13151  ismnd  13582  sgrpidmndm  13583  dfgrp3me  13763  issubg2m  13856  subrgintm  14338  islssm  14453  islidlm  14575  neipsm  14965  dedekindeulemub  15429  dedekindeulemloc  15430  dedekindeulemlub  15431  suplociccex  15436  dedekindicclemub  15438  dedekindicclemloc  15439  dedekindicclemlub  15440  limcimo  15476  dvmptfsum  15536  elply2  15546  lgsval  15823  lgsdir  15854  lgsdilem2  15855  lgsdi  15856  lgsne0  15857  lgsquadlem3  15898  lgsquad  15899  2sqlem8  15942  bj-charfunbi  16527