Theorem eleq1w 2257

Description: Weaker version of eleq1 2259 (but more general than elequ1 2171) not depending on ax-ext 2178 nor df-cleq 2189. (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 1727	. . . 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 1839	. 2 |- ( x = y -> ( E. z ( z = x /\ z e. A ) <-> E. z ( z = y /\ z e. A ) ) )
4		df-clel 2192	. 2 |- ( x e. A <-> E. z ( z = x /\ z e. A ) )
5		df-clel 2192	. 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 1506   e. wcel 2167

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548

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

This theorem is referenced by:  clelsb1f  2343  cbvralfw  2719  cbvrexfw  2720  cbvralvw  2733  cbvrexvw  2734  cbvreuvw  2735  dfdif3  3274  dfss4st  3397  abn0m  3477  r19.2m  3538  cbvmptf  4128  iinexgm  4188  xpiindim  4804  cnviinm  5212  iotam  5251  elfvm  5594  uchoice  6204  iinerm  6675  ixpiinm  6792  ixpsnf1o  6804  mapsnen  6879  pw2f1odclem  6904  enumctlemm  7189  nnnninfeq  7203  exmidomni  7217  fodjum  7221  finacn  7287  exmidontriimlem4  7307  exmidontriim  7308  cc2  7350  suplocexprlemmu  7802  suplocsr  7893  axpre-suploc  7986  suprzubdc  10343  nninfdcex  10344  zsupssdc  10345  iseqf1olemqk  10616  seq3f1olemqsum  10622  summodclem2  11564  summodc  11565  zsumdc  11566  fsum3  11569  isumz  11571  isumss  11573  fisumss  11574  isumss2  11575  fsum3cvg2  11576  fsumsersdc  11577  fsum3ser  11579  fsumsplit  11589  fsumsplitf  11590  isumlessdc  11678  prodfdivap  11729  cbvprod  11740  prodrbdclem  11753  prodmodclem2  11759  prodmodc  11760  zproddc  11761  fprodseq  11765  fprodntrivap  11766  prod1dc  11768  prodssdc  11771  fprodsplitdc  11778  fprod2dlemstep  11804  fproddivapf  11813  fprodsplitf  11814  nnmindc  12226  nnminle  12227  nninfctlemfo  12232  pcmptdvds  12539  nninfdclemp1  12692  ismnd  13121  sgrpidmndm  13122  dfgrp3me  13302  issubg2m  13395  subrgintm  13875  islssm  13989  islidlm  14111  neipsm  14474  dedekindeulemub  14938  dedekindeulemloc  14939  dedekindeulemlub  14940  suplociccex  14945  dedekindicclemub  14947  dedekindicclemloc  14948  dedekindicclemlub  14949  limcimo  14985  dvmptfsum  15045  elply2  15055  lgsval  15329  lgsdir  15360  lgsdilem2  15361  lgsdi  15362  lgsne0  15363  lgsquadlem3  15404  lgsquad  15405  2sqlem8  15448  bj-charfunbi  15541