Theorem eleq1w 2254

Description: Weaker version of eleq1 2256 (but more general than elequ1 2168) not depending on ax-ext 2175 nor df-cleq 2186. (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 1724	. . . 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 1836	. 2 |- ( x = y -> ( E. z ( z = x /\ z e. A ) <-> E. z ( z = y /\ z e. A ) ) )
4		df-clel 2189	. 2 |- ( x e. A <-> E. z ( z = x /\ z e. A ) )
5		df-clel 2189	. 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 1503   e. wcel 2164

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545

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

This theorem is referenced by:  clelsb1f  2340  cbvralfw  2716  cbvrexfw  2717  cbvralvw  2730  cbvrexvw  2731  cbvreuvw  2732  dfdif3  3269  dfss4st  3392  abn0m  3472  r19.2m  3533  cbvmptf  4123  iinexgm  4183  xpiindim  4799  cnviinm  5207  iotam  5246  elfvm  5587  uchoice  6190  iinerm  6661  ixpiinm  6778  ixpsnf1o  6790  mapsnen  6865  pw2f1odclem  6890  enumctlemm  7173  nnnninfeq  7187  exmidomni  7201  fodjum  7205  exmidontriimlem4  7284  exmidontriim  7285  cc2  7327  suplocexprlemmu  7778  suplocsr  7869  axpre-suploc  7962  iseqf1olemqk  10578  seq3f1olemqsum  10584  summodclem2  11525  summodc  11526  zsumdc  11527  fsum3  11530  isumz  11532  isumss  11534  fisumss  11535  isumss2  11536  fsum3cvg2  11537  fsumsersdc  11538  fsum3ser  11540  fsumsplit  11550  fsumsplitf  11551  isumlessdc  11639  prodfdivap  11690  cbvprod  11701  prodrbdclem  11714  prodmodclem2  11720  prodmodc  11721  zproddc  11722  fprodseq  11726  fprodntrivap  11727  prod1dc  11729  prodssdc  11732  fprodsplitdc  11739  fprod2dlemstep  11765  fproddivapf  11774  fprodsplitf  11775  suprzubdc  12089  nninfdcex  12090  zsupssdc  12091  nnmindc  12171  nnminle  12172  nninfctlemfo  12177  pcmptdvds  12483  nninfdclemp1  12607  ismnd  13000  sgrpidmndm  13001  dfgrp3me  13172  issubg2m  13259  subrgintm  13739  islssm  13853  islidlm  13975  neipsm  14322  dedekindeulemub  14772  dedekindeulemloc  14773  dedekindeulemlub  14774  suplociccex  14779  dedekindicclemub  14781  dedekindicclemloc  14782  dedekindicclemlub  14783  limcimo  14819  elply2  14881  lgsval  15120  lgsdir  15151  lgsdilem2  15152  lgsdi  15153  lgsne0  15154  2sqlem8  15210  bj-charfunbi  15303