Theorem eleq1w 2238

Description: Weaker version of eleq1 2240 (but more general than elequ1 2152) not depending on ax-ext 2159 nor df-cleq 2170. (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 1713	. . . 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 1825	. 2 |- ( x = y -> ( E. z ( z = x /\ z e. A ) <-> E. z ( z = y /\ z e. A ) ) )
4		df-clel 2173	. 2 |- ( x e. A <-> E. z ( z = x /\ z e. A ) )
5		df-clel 2173	. 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 1492   e. wcel 2148

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534

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

This theorem is referenced by:  clelsb1f  2323  cbvralfw  2694  cbvrexfw  2695  cbvralvw  2707  cbvrexvw  2708  cbvreuvw  2709  dfdif3  3245  dfss4st  3368  abn0m  3448  r19.2m  3509  cbvmptf  4097  iinexgm  4154  xpiindim  4764  cnviinm  5170  iotam  5208  iinerm  6606  ixpiinm  6723  ixpsnf1o  6735  mapsnen  6810  enumctlemm  7112  nnnninfeq  7125  exmidomni  7139  fodjum  7143  exmidontriimlem4  7222  exmidontriim  7223  cc2  7265  suplocexprlemmu  7716  suplocsr  7807  axpre-suploc  7900  iseqf1olemqk  10493  seq3f1olemqsum  10499  summodclem2  11389  summodc  11390  zsumdc  11391  fsum3  11394  isumz  11396  isumss  11398  fisumss  11399  isumss2  11400  fsum3cvg2  11401  fsumsersdc  11402  fsum3ser  11404  fsumsplit  11414  fsumsplitf  11415  isumlessdc  11503  prodfdivap  11554  cbvprod  11565  prodrbdclem  11578  prodmodclem2  11584  prodmodc  11585  zproddc  11586  fprodseq  11590  fprodntrivap  11591  prod1dc  11593  prodssdc  11596  fprodsplitdc  11603  fprod2dlemstep  11629  fproddivapf  11638  fprodsplitf  11639  suprzubdc  11952  nninfdcex  11953  zsupssdc  11954  nnmindc  12034  nnminle  12035  pcmptdvds  12342  nninfdclemcl  12448  nninfdclemp1  12450  ismnd  12819  sgrpidmndm  12820  dfgrp3me  12969  issubg2m  13047  subrgintm  13362  neipsm  13624  dedekindeulemub  14066  dedekindeulemloc  14067  dedekindeulemlub  14068  suplociccex  14073  dedekindicclemub  14075  dedekindicclemloc  14076  dedekindicclemlub  14077  limcimo  14104  lgsval  14375  lgsdir  14406  lgsdilem2  14407  lgsdi  14408  lgsne0  14409  2sqlem8  14440  bj-charfunbi  14533