Theorem eleq1w 2290

Description: Weaker version of eleq1 2292 (but more general than elequ1 2204) not depending on ax-ext 2211 nor df-cleq 2222. (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 1759	. . . 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 1871	. 2 |- ( x = y -> ( E. z ( z = x /\ z e. A ) <-> E. z ( z = y /\ z e. A ) ) )
4		df-clel 2225	. 2 |- ( x e. A <-> E. z ( z = x /\ z e. A ) )
5		df-clel 2225	. 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 1538   e. wcel 2200

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580

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

This theorem is referenced by:  clelsb1f  2376  cbvrmow  2714  cbvralfw  2754  cbvrexfw  2755  cbvralvw  2769  cbvrexvw  2770  cbvreuvw  2771  dfdif3  3314  dfss4st  3437  abn0m  3517  r19.2m  3578  cbvmptf  4178  iinexgm  4238  xpiindim  4859  reldmm  4942  cnviinm  5270  iotam  5310  elfvm  5660  cbvriotavw  5965  uchoice  6283  iinerm  6754  ixpiinm  6871  ixpsnf1o  6883  mapsnen  6964  pw2f1odclem  6995  enumctlemm  7281  nnnninfeq  7295  exmidomni  7309  fodjum  7313  finacn  7386  exmidontriimlem4  7406  exmidontriim  7407  cc2  7453  suplocexprlemmu  7905  suplocsr  7996  axpre-suploc  8089  suprzubdc  10456  nninfdcex  10457  zsupssdc  10458  iseqf1olemqk  10729  seq3f1olemqsum  10735  reuccatpfxs1  11279  summodclem2  11893  summodc  11894  zsumdc  11895  fsum3  11898  isumz  11900  isumss  11902  fisumss  11903  isumss2  11904  fsum3cvg2  11905  fsumsersdc  11906  fsum3ser  11908  fsumsplit  11918  fsumsplitf  11919  isumlessdc  12007  prodfdivap  12058  cbvprod  12069  prodrbdclem  12082  prodmodclem2  12088  prodmodc  12089  zproddc  12090  fprodseq  12094  fprodntrivap  12095  prod1dc  12097  prodssdc  12100  fprodsplitdc  12107  fprod2dlemstep  12133  fproddivapf  12142  fprodsplitf  12143  nnmindc  12555  nnminle  12556  nninfctlemfo  12561  pcmptdvds  12868  nninfdclemp1  13021  ismnd  13452  sgrpidmndm  13453  dfgrp3me  13633  issubg2m  13726  subrgintm  14207  islssm  14321  islidlm  14443  neipsm  14828  dedekindeulemub  15292  dedekindeulemloc  15293  dedekindeulemlub  15294  suplociccex  15299  dedekindicclemub  15301  dedekindicclemloc  15302  dedekindicclemlub  15303  limcimo  15339  dvmptfsum  15399  elply2  15409  lgsval  15683  lgsdir  15714  lgsdilem2  15715  lgsdi  15716  lgsne0  15717  lgsquadlem3  15758  lgsquad  15759  2sqlem8  15802  bj-charfunbi  16174