Theorem eleq1w 2293

Description: Weaker version of eleq1 2295 (but more general than elequ1 2207) not depending on ax-ext 2214 nor df-cleq 2225. (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 2228	. 2 ⊢ (𝑥 ∈ 𝐴 ↔ ∃𝑧(𝑧 = 𝑥 ∧ 𝑧 ∈ 𝐴))
5		df-clel 2228	. 2 ⊢ (𝑦 ∈ 𝐴 ↔ ∃𝑧(𝑧 = 𝑦 ∧ 𝑧 ∈ 𝐴))
6	3, 4, 5	3bitr4g 223	1 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))

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

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 2228

This theorem is referenced by:  clelsb1f  2388  cbvrmow  2727  cbvralfw  2767  cbvrexfw  2768  cbvralvw  2782  cbvrexvw  2783  cbvreuvw  2784  dfdif3  3329  dfss4st  3454  abn0m  3534  r19.2m  3596  rabsnifsb  3757  cbvmptf  4204  iinexgm  4266  xpiindim  4892  reldmm  4975  cnviinm  5304  iotam  5344  elfvm  5703  cbvriotavw  6014  uchoice  6331  suppssdc  6460  iinerm  6841  ixpiinm  6959  ixpsnf1o  6971  mapsnend  7052  mapsnen  7053  pw2f1odclem  7087  enumctlemm  7405  nnnninfeq  7419  exmidomni  7433  fodjum  7437  finacn  7511  exmidontriimlem4  7531  exmidontriim  7532  cc2  7581  suplocexprlemmu  8033  suplocsr  8124  axpre-suploc  8217  suprzubdc  10596  nninfdcex  10597  zsupssdc  10598  iseqf1olemqk  10869  seq3f1olemqsum  10875  reuccatpfxs1  11439  summodclem2  12068  summodc  12069  zsumdc  12070  fsum3  12073  isumz  12075  isumss  12077  fisumss  12078  isumss2  12079  fsum3cvg2  12080  fsumsersdc  12081  fsum3ser  12083  fsumsplit  12093  fsumsplitf  12094  isumlessdc  12182  prodfdivap  12233  cbvprod  12244  prodrbdclem  12257  prodmodclem2  12263  prodmodc  12264  zproddc  12265  fprodseq  12269  fprodntrivap  12270  prod1dc  12272  prodssdc  12275  fprodsplitdc  12282  fprod2dlemstep  12308  fproddivapf  12317  fprodsplitf  12318  nnmindc  12730  nnminle  12731  nninfctlemfo  12736  pcmptdvds  13043  nninfdclemp1  13201  ismnd  13632  sgrpidmndm  13633  dfgrp3me  13813  issubg2m  13906  subrgintm  14388  islssm  14505  islidlm  14627  neipsm  15019  dedekindeulemub  15483  dedekindeulemloc  15484  dedekindeulemlub  15485  suplociccex  15490  dedekindicclemub  15492  dedekindicclemloc  15493  dedekindicclemlub  15494  limcimo  15530  dvmptfsum  15590  elply2  15600  lgsval  15877  lgsdir  15908  lgsdilem2  15909  lgsdi  15910  lgsne0  15911  lgsquadlem3  15952  lgsquad  15953  2sqlem8  15996  bj-charfunbi  16581