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	⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))

Proof of Theorem eleq1w

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		equequ2 1759	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 ↔ 𝑧 = 𝑦))
2	1	anbi1d 465	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑧 = 𝑥 ∧ 𝑧 ∈ 𝐴) ↔ (𝑧 = 𝑦 ∧ 𝑧 ∈ 𝐴)))
3	2	exbidv 1871	. 2 ⊢ (𝑥 = 𝑦 → (∃𝑧(𝑧 = 𝑥 ∧ 𝑧 ∈ 𝐴) ↔ ∃𝑧(𝑧 = 𝑦 ∧ 𝑧 ∈ 𝐴)))
4		df-clel 2225	. 2 ⊢ (𝑥 ∈ 𝐴 ↔ ∃𝑧(𝑧 = 𝑥 ∧ 𝑧 ∈ 𝐴))
5		df-clel 2225	. 2 ⊢ (𝑦 ∈ 𝐴 ↔ ∃𝑧(𝑧 = 𝑦 ∧ 𝑧 ∈ 𝐴))
6	3, 4, 5	3bitr4g 223	1 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105  ∃wex 1538   ∈ 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  5662  cbvriotavw  5971  uchoice  6289  iinerm  6762  ixpiinm  6879  ixpsnf1o  6891  mapsnen  6972  pw2f1odclem  7003  enumctlemm  7292  nnnninfeq  7306  exmidomni  7320  fodjum  7324  finacn  7397  exmidontriimlem4  7417  exmidontriim  7418  cc2  7464  suplocexprlemmu  7916  suplocsr  8007  axpre-suploc  8100  suprzubdc  10468  nninfdcex  10469  zsupssdc  10470  iseqf1olemqk  10741  seq3f1olemqsum  10747  reuccatpfxs1  11294  summodclem2  11908  summodc  11909  zsumdc  11910  fsum3  11913  isumz  11915  isumss  11917  fisumss  11918  isumss2  11919  fsum3cvg2  11920  fsumsersdc  11921  fsum3ser  11923  fsumsplit  11933  fsumsplitf  11934  isumlessdc  12022  prodfdivap  12073  cbvprod  12084  prodrbdclem  12097  prodmodclem2  12103  prodmodc  12104  zproddc  12105  fprodseq  12109  fprodntrivap  12110  prod1dc  12112  prodssdc  12115  fprodsplitdc  12122  fprod2dlemstep  12148  fproddivapf  12157  fprodsplitf  12158  nnmindc  12570  nnminle  12571  nninfctlemfo  12576  pcmptdvds  12883  nninfdclemp1  13036  ismnd  13467  sgrpidmndm  13468  dfgrp3me  13648  issubg2m  13741  subrgintm  14222  islssm  14336  islidlm  14458  neipsm  14843  dedekindeulemub  15307  dedekindeulemloc  15308  dedekindeulemlub  15309  suplociccex  15314  dedekindicclemub  15316  dedekindicclemloc  15317  dedekindicclemlub  15318  limcimo  15354  dvmptfsum  15414  elply2  15424  lgsval  15698  lgsdir  15729  lgsdilem2  15730  lgsdi  15731  lgsne0  15732  lgsquadlem3  15773  lgsquad  15774  2sqlem8  15817  bj-charfunbi  16229