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  4225  iinexgm  4290  xpiindim  4917  reldmm  5000  cnviinm  5329  iotam  5369  elfvm  5729  mptmex  5945  cbvriotavw  6049  uchoice  6371  suppssdc  6500  iinerm  6881  ixpiinm  7006  ixpsnf1o  7018  mapsnend  7099  mapsnen  7100  pw2f1odclem  7134  enumctlemm  7455  nnnninfeq  7469  exmidomni  7483  fodjum  7487  finacn  7561  exmidontriimlem4  7581  exmidontriim  7582  cc2  7634  suplocexprlemmu  8086  suplocsr  8177  axpre-suploc  8270  indfdc  9301  suprzubdc  10682  nninfdcex  10683  zsupssdc  10684  iseqf1olemqk  10959  seq3f1olemqsum  10965  reuccatpfxs1  11535  summodclem2  12168  summodc  12169  zsumdc  12170  fsum3  12173  isumz  12175  isumss  12177  fisumss  12178  isumss2  12179  fsum3cvg2  12180  fsumsersdc  12181  fsum3ser  12183  fsumsplit  12193  fsumsplitf  12194  isumlessdc  12282  prodfdivap  12333  cbvprod  12344  prodrbdclem  12357  prodmodclem2  12363  prodmodc  12364  zproddc  12365  fprodseq  12369  fprodntrivap  12370  prod1dc  12372  prodssdc  12375  fprodsplitdc  12382  fprod2dlemstep  12408  fproddivapf  12417  fprodsplitf  12418  nnmindc  12830  nnminle  12831  nninfctlemfo  12836  pcmptdvds  13147  nninfdclemp1  13393  ismnd  13785  sgrpidmndm  13786  dfgrp3me  13958  issubg2m  14045  subrgintm  14635  islssm  14778  islidlm  14900  neipsm  15346  dedekindeulemub  15810  dedekindeulemloc  15811  dedekindeulemlub  15812  suplociccex  15817  dedekindicclemub  15819  dedekindicclemloc  15820  dedekindicclemlub  15821  limcimo  15857  dvmptfsum  15917  elply2  15927  prmorcht  16243  lgsval  16289  lgsdir  16320  lgsdilem2  16321  lgsdi  16322  lgsne0  16323  lgsquadlem3  16364  lgsquad  16365  2sqlem8  16408  bj-charfunbi  17003  2alsraln0idm  17326