Theorem eleq1w 2299

Description: Weaker version of eleq1 2301 (but more general than elequ1 2213) not depending on ax-ext 2220 nor df-cleq 2231. (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 1765	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 ↔ 𝑧 = 𝑦))
2	1	anbi1d 469	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑧 = 𝑥 ∧ 𝑧 ∈ 𝐴) ↔ (𝑧 = 𝑦 ∧ 𝑧 ∈ 𝐴)))
3	2	exbidv 1878	. 2 ⊢ (𝑥 = 𝑦 → (∃𝑧(𝑧 = 𝑥 ∧ 𝑧 ∈ 𝐴) ↔ ∃𝑧(𝑧 = 𝑦 ∧ 𝑧 ∈ 𝐴)))
4		df-clel 2234	. 2 ⊢ (𝑥 ∈ 𝐴 ↔ ∃𝑧(𝑧 = 𝑥 ∧ 𝑧 ∈ 𝐴))
5		df-clel 2234	. 2 ⊢ (𝑦 ∈ 𝐴 ↔ ∃𝑧(𝑧 = 𝑦 ∧ 𝑧 ∈ 𝐴))
6	3, 4, 5	3bitr4g 223	1 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ↔ wb 105  ∃wex 1545   ∈ wcel 2209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587

This proof depends on definitions:  df-bi 117  df-clel 2234

This theorem is used by:  clelsb1f  2396  cbvrmow  2735  cbvralfw  2775  cbvrexfw  2776  cbvralvw  2790  cbvrexvw  2791  cbvreuvw  2792  dfdif3  3339  dfss4st  3464  abn0m  3547  r19.2m  3614  rabsnifsb  3777  cbvmptf  4227  iinexgm  4292  xpiindim  4919  reldmm  5002  cnviinm  5332  iotam  5372  elfvm  5732  mptmex  5948  cbvriotavw  6052  uchoice  6375  suppssdc  6504  iinerm  6885  ixpiinm  7010  ixpsnf1o  7022  mapsnend  7103  mapsnen  7104  pw2f1odclem  7138  enumctlemm  7460  nnnninfeq  7474  exmidomni  7488  fodjum  7492  finacn  7566  exmidontriimlem4  7586  exmidontriim  7587  cc2  7639  suplocexprlemmu  8091  suplocsr  8182  axpre-suploc  8275  indfdc  9307  suprzubdc  10688  nninfdcex  10689  zsupssdc  10690  iseqf1olemqk  10965  seq3f1olemqsum  10971  reuccatpfxs1  11541  summodclem2  12174  summodc  12175  zsumdc  12176  fsum3  12179  isumz  12181  isumss  12183  fisumss  12184  isumss2  12185  fsum3cvg2  12186  fsumsersdc  12187  fsum3ser  12189  fsumsplit  12199  fsumsplitf  12200  isumlessdc  12288  prodfdivap  12339  cbvprod  12350  prodrbdclem  12363  prodmodclem2  12369  prodmodc  12370  zproddc  12371  fprodseq  12375  fprodntrivap  12376  prod1dc  12378  prodssdc  12381  fprodsplitdc  12388  fprod2dlemstep  12414  fproddivapf  12423  fprodsplitf  12424  nnmindc  12836  nnminle  12837  nninfctlemfo  12842  pcmptdvds  13153  nninfdclemp1  13399  ismnd  13791  sgrpidmndm  13792  dfgrp3me  13964  issubg2m  14051  gsumresfi  14263  subrgintm  14660  islssm  14803  islidlm  14925  neipsm  15380  dedekindeulemub  15844  dedekindeulemloc  15845  dedekindeulemlub  15846  suplociccex  15851  dedekindicclemub  15853  dedekindicclemloc  15854  dedekindicclemlub  15855  limcimo  15891  dvmptfsum  15951  elply2  15961  prmorcht  16282  lgsval  16328  lgsdir  16359  lgsdilem2  16360  lgsdi  16361  lgsne0  16362  lgsquadlem3  16403  lgsquad  16404  2sqlem8  16447  bj-charfunbi  17042  2alsraln0idm  17366