Theorem eleq1w 2295

Description: Weaker version of eleq1 2297 (but more general than elequ1 2209) not depending on ax-ext 2216 nor df-cleq 2227. (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 1761	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 ↔ 𝑧 = 𝑦))
2	1	anbi1d 465	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑧 = 𝑥 ∧ 𝑧 ∈ 𝐴) ↔ (𝑧 = 𝑦 ∧ 𝑧 ∈ 𝐴)))
3	2	exbidv 1874	. 2 ⊢ (𝑥 = 𝑦 → (∃𝑧(𝑧 = 𝑥 ∧ 𝑧 ∈ 𝐴) ↔ ∃𝑧(𝑧 = 𝑦 ∧ 𝑧 ∈ 𝐴)))
4		df-clel 2230	. 2 ⊢ (𝑥 ∈ 𝐴 ↔ ∃𝑧(𝑧 = 𝑥 ∧ 𝑧 ∈ 𝐴))
5		df-clel 2230	. 2 ⊢ (𝑦 ∈ 𝐴 ↔ ∃𝑧(𝑧 = 𝑦 ∧ 𝑧 ∈ 𝐴))
6	3, 4, 5	3bitr4g 223	1 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105  ∃wex 1541   ∈ wcel 2205

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583

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

This theorem is referenced by:  clelsb1f  2390  cbvrmow  2729  cbvralfw  2769  cbvrexfw  2770  cbvralvw  2784  cbvrexvw  2785  cbvreuvw  2786  dfdif3  3333  dfss4st  3458  abn0m  3538  r19.2m  3600  rabsnifsb  3762  cbvmptf  4209  iinexgm  4271  xpiindim  4897  reldmm  4980  cnviinm  5309  iotam  5349  elfvm  5708  cbvriotavw  6022  uchoice  6344  suppssdc  6473  iinerm  6854  ixpiinm  6972  ixpsnf1o  6984  mapsnend  7065  mapsnen  7066  pw2f1odclem  7100  enumctlemm  7418  nnnninfeq  7432  exmidomni  7446  fodjum  7450  finacn  7524  exmidontriimlem4  7544  exmidontriim  7545  cc2  7597  suplocexprlemmu  8049  suplocsr  8140  axpre-suploc  8233  suprzubdc  10620  nninfdcex  10621  zsupssdc  10622  iseqf1olemqk  10893  seq3f1olemqsum  10899  reuccatpfxs1  11464  summodclem2  12093  summodc  12094  zsumdc  12095  fsum3  12098  isumz  12100  isumss  12102  fisumss  12103  isumss2  12104  fsum3cvg2  12105  fsumsersdc  12106  fsum3ser  12108  fsumsplit  12118  fsumsplitf  12119  isumlessdc  12207  prodfdivap  12258  cbvprod  12269  prodrbdclem  12282  prodmodclem2  12288  prodmodc  12289  zproddc  12290  fprodseq  12294  fprodntrivap  12295  prod1dc  12297  prodssdc  12300  fprodsplitdc  12307  fprod2dlemstep  12333  fproddivapf  12342  fprodsplitf  12343  nnmindc  12755  nnminle  12756  nninfctlemfo  12761  pcmptdvds  13068  nninfdclemp1  13285  ismnd  13680  sgrpidmndm  13681  dfgrp3me  13855  issubg2m  13942  subrgintm  14489  islssm  14631  islidlm  14753  neipsm  15145  dedekindeulemub  15609  dedekindeulemloc  15610  dedekindeulemlub  15611  suplociccex  15616  dedekindicclemub  15618  dedekindicclemloc  15619  dedekindicclemlub  15620  limcimo  15656  dvmptfsum  15716  elply2  15726  lgsval  16003  lgsdir  16034  lgsdilem2  16035  lgsdi  16036  lgsne0  16037  lgsquadlem3  16078  lgsquad  16079  2sqlem8  16122  bj-charfunbi  16707