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  5981  uchoice  6299  iinerm  6775  ixpiinm  6892  ixpsnf1o  6904  mapsnen  6985  pw2f1odclem  7019  enumctlemm  7312  nnnninfeq  7326  exmidomni  7340  fodjum  7344  finacn  7418  exmidontriimlem4  7438  exmidontriim  7439  cc2  7485  suplocexprlemmu  7937  suplocsr  8028  axpre-suploc  8121  suprzubdc  10495  nninfdcex  10496  zsupssdc  10497  iseqf1olemqk  10768  seq3f1olemqsum  10774  reuccatpfxs1  11327  summodclem2  11942  summodc  11943  zsumdc  11944  fsum3  11947  isumz  11949  isumss  11951  fisumss  11952  isumss2  11953  fsum3cvg2  11954  fsumsersdc  11955  fsum3ser  11957  fsumsplit  11967  fsumsplitf  11968  isumlessdc  12056  prodfdivap  12107  cbvprod  12118  prodrbdclem  12131  prodmodclem2  12137  prodmodc  12138  zproddc  12139  fprodseq  12143  fprodntrivap  12144  prod1dc  12146  prodssdc  12149  fprodsplitdc  12156  fprod2dlemstep  12182  fproddivapf  12191  fprodsplitf  12192  nnmindc  12604  nnminle  12605  nninfctlemfo  12610  pcmptdvds  12917  nninfdclemp1  13070  ismnd  13501  sgrpidmndm  13502  dfgrp3me  13682  issubg2m  13775  subrgintm  14256  islssm  14370  islidlm  14492  neipsm  14877  dedekindeulemub  15341  dedekindeulemloc  15342  dedekindeulemlub  15343  suplociccex  15348  dedekindicclemub  15350  dedekindicclemloc  15351  dedekindicclemlub  15352  limcimo  15388  dvmptfsum  15448  elply2  15458  lgsval  15732  lgsdir  15763  lgsdilem2  15764  lgsdi  15765  lgsne0  15766  lgsquadlem3  15807  lgsquad  15808  2sqlem8  15851  bj-charfunbi  16406