Theorem eleq1w 2292

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

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

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582

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

This theorem is referenced by:  clelsb1f  2378  cbvrmow  2716  cbvralfw  2756  cbvrexfw  2757  cbvralvw  2771  cbvrexvw  2772  cbvreuvw  2773  dfdif3  3317  dfss4st  3440  abn0m  3520  r19.2m  3581  rabsnifsb  3737  cbvmptf  4183  iinexgm  4244  xpiindim  4867  reldmm  4950  cnviinm  5278  iotam  5318  elfvm  5672  cbvriotavw  5982  uchoice  6300  iinerm  6776  ixpiinm  6893  ixpsnf1o  6905  mapsnen  6986  pw2f1odclem  7020  enumctlemm  7313  nnnninfeq  7327  exmidomni  7341  fodjum  7345  finacn  7419  exmidontriimlem4  7439  exmidontriim  7440  cc2  7486  suplocexprlemmu  7938  suplocsr  8029  axpre-suploc  8122  suprzubdc  10497  nninfdcex  10498  zsupssdc  10499  iseqf1olemqk  10770  seq3f1olemqsum  10776  reuccatpfxs1  11332  summodclem2  11948  summodc  11949  zsumdc  11950  fsum3  11953  isumz  11955  isumss  11957  fisumss  11958  isumss2  11959  fsum3cvg2  11960  fsumsersdc  11961  fsum3ser  11963  fsumsplit  11973  fsumsplitf  11974  isumlessdc  12062  prodfdivap  12113  cbvprod  12124  prodrbdclem  12137  prodmodclem2  12143  prodmodc  12144  zproddc  12145  fprodseq  12149  fprodntrivap  12150  prod1dc  12152  prodssdc  12155  fprodsplitdc  12162  fprod2dlemstep  12188  fproddivapf  12197  fprodsplitf  12198  nnmindc  12610  nnminle  12611  nninfctlemfo  12616  pcmptdvds  12923  nninfdclemp1  13076  ismnd  13507  sgrpidmndm  13508  dfgrp3me  13688  issubg2m  13781  subrgintm  14263  islssm  14377  islidlm  14499  neipsm  14884  dedekindeulemub  15348  dedekindeulemloc  15349  dedekindeulemlub  15350  suplociccex  15355  dedekindicclemub  15357  dedekindicclemloc  15358  dedekindicclemlub  15359  limcimo  15395  dvmptfsum  15455  elply2  15465  lgsval  15739  lgsdir  15770  lgsdilem2  15771  lgsdi  15772  lgsne0  15773  lgsquadlem3  15814  lgsquad  15815  2sqlem8  15858  bj-charfunbi  16432