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 1541   ∈ 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 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 2227

This theorem is referenced by:  clelsb1f  2379  cbvrmow  2717  cbvralfw  2757  cbvrexfw  2758  cbvralvw  2772  cbvrexvw  2773  cbvreuvw  2774  dfdif3  3319  dfss4st  3442  abn0m  3522  r19.2m  3583  rabsnifsb  3741  cbvmptf  4188  iinexgm  4249  xpiindim  4873  reldmm  4956  cnviinm  5285  iotam  5325  elfvm  5681  cbvriotavw  5992  uchoice  6309  suppssdc  6438  iinerm  6819  ixpiinm  6936  ixpsnf1o  6948  mapsnen  7029  pw2f1odclem  7063  enumctlemm  7356  nnnninfeq  7370  exmidomni  7384  fodjum  7388  finacn  7462  exmidontriimlem4  7482  exmidontriim  7483  cc2  7529  suplocexprlemmu  7981  suplocsr  8072  axpre-suploc  8165  suprzubdc  10542  nninfdcex  10543  zsupssdc  10544  iseqf1olemqk  10815  seq3f1olemqsum  10821  reuccatpfxs1  11377  summodclem2  12006  summodc  12007  zsumdc  12008  fsum3  12011  isumz  12013  isumss  12015  fisumss  12016  isumss2  12017  fsum3cvg2  12018  fsumsersdc  12019  fsum3ser  12021  fsumsplit  12031  fsumsplitf  12032  isumlessdc  12120  prodfdivap  12171  cbvprod  12182  prodrbdclem  12195  prodmodclem2  12201  prodmodc  12202  zproddc  12203  fprodseq  12207  fprodntrivap  12208  prod1dc  12210  prodssdc  12213  fprodsplitdc  12220  fprod2dlemstep  12246  fproddivapf  12255  fprodsplitf  12256  nnmindc  12668  nnminle  12669  nninfctlemfo  12674  pcmptdvds  12981  nninfdclemp1  13134  ismnd  13565  sgrpidmndm  13566  dfgrp3me  13746  issubg2m  13839  subrgintm  14321  islssm  14436  islidlm  14558  neipsm  14948  dedekindeulemub  15412  dedekindeulemloc  15413  dedekindeulemlub  15414  suplociccex  15419  dedekindicclemub  15421  dedekindicclemloc  15422  dedekindicclemlub  15423  limcimo  15459  dvmptfsum  15519  elply2  15529  lgsval  15806  lgsdir  15837  lgsdilem2  15838  lgsdi  15839  lgsne0  15840  lgsquadlem3  15881  lgsquad  15882  2sqlem8  15925  bj-charfunbi  16510