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  3331  dfss4st  3456  abn0m  3536  r19.2m  3598  rabsnifsb  3759  cbvmptf  4206  iinexgm  4268  xpiindim  4894  reldmm  4977  cnviinm  5306  iotam  5346  elfvm  5705  cbvriotavw  6016  uchoice  6333  suppssdc  6462  iinerm  6843  ixpiinm  6961  ixpsnf1o  6973  mapsnend  7054  mapsnen  7055  pw2f1odclem  7089  enumctlemm  7407  nnnninfeq  7421  exmidomni  7435  fodjum  7439  finacn  7513  exmidontriimlem4  7533  exmidontriim  7534  cc2  7583  suplocexprlemmu  8035  suplocsr  8126  axpre-suploc  8219  suprzubdc  10600  nninfdcex  10601  zsupssdc  10602  iseqf1olemqk  10873  seq3f1olemqsum  10879  reuccatpfxs1  11443  summodclem2  12072  summodc  12073  zsumdc  12074  fsum3  12077  isumz  12079  isumss  12081  fisumss  12082  isumss2  12083  fsum3cvg2  12084  fsumsersdc  12085  fsum3ser  12087  fsumsplit  12097  fsumsplitf  12098  isumlessdc  12186  prodfdivap  12237  cbvprod  12248  prodrbdclem  12261  prodmodclem2  12267  prodmodc  12268  zproddc  12269  fprodseq  12273  fprodntrivap  12274  prod1dc  12276  prodssdc  12279  fprodsplitdc  12286  fprod2dlemstep  12312  fproddivapf  12321  fprodsplitf  12322  nnmindc  12734  nnminle  12735  nninfctlemfo  12740  pcmptdvds  13047  nninfdclemp1  13218  ismnd  13649  sgrpidmndm  13650  dfgrp3me  13830  issubg2m  13923  subrgintm  14405  islssm  14522  islidlm  14644  neipsm  15036  dedekindeulemub  15500  dedekindeulemloc  15501  dedekindeulemlub  15502  suplociccex  15507  dedekindicclemub  15509  dedekindicclemloc  15510  dedekindicclemlub  15511  limcimo  15547  dvmptfsum  15607  elply2  15617  lgsval  15894  lgsdir  15925  lgsdilem2  15926  lgsdi  15927  lgsne0  15928  lgsquadlem3  15969  lgsquad  15970  2sqlem8  16013  bj-charfunbi  16598