Theorem eleq1w 2236

Description: Weaker version of eleq1 2238 (but more general than elequ1 2150) not depending on ax-ext 2157 nor df-cleq 2168. (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 1711	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 ↔ 𝑧 = 𝑦))
2	1	anbi1d 465	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑧 = 𝑥 ∧ 𝑧 ∈ 𝐴) ↔ (𝑧 = 𝑦 ∧ 𝑧 ∈ 𝐴)))
3	2	exbidv 1823	. 2 ⊢ (𝑥 = 𝑦 → (∃𝑧(𝑧 = 𝑥 ∧ 𝑧 ∈ 𝐴) ↔ ∃𝑧(𝑧 = 𝑦 ∧ 𝑧 ∈ 𝐴)))
4		df-clel 2171	. 2 ⊢ (𝑥 ∈ 𝐴 ↔ ∃𝑧(𝑧 = 𝑥 ∧ 𝑧 ∈ 𝐴))
5		df-clel 2171	. 2 ⊢ (𝑦 ∈ 𝐴 ↔ ∃𝑧(𝑧 = 𝑦 ∧ 𝑧 ∈ 𝐴))
6	3, 4, 5	3bitr4g 223	1 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))

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

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 1445  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532

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

This theorem is referenced by:  clelsb1f  2321  cbvralfw  2692  cbvrexfw  2693  cbvralvw  2705  cbvrexvw  2706  cbvreuvw  2707  dfdif3  3243  dfss4st  3366  abn0m  3446  r19.2m  3507  cbvmptf  4092  iinexgm  4149  xpiindim  4757  cnviinm  5162  iotam  5200  iinerm  6597  ixpiinm  6714  ixpsnf1o  6726  mapsnen  6801  enumctlemm  7103  nnnninfeq  7116  exmidomni  7130  fodjum  7134  exmidontriimlem4  7213  exmidontriim  7214  cc2  7241  suplocexprlemmu  7692  suplocsr  7783  axpre-suploc  7876  iseqf1olemqk  10462  seq3f1olemqsum  10468  summodclem2  11356  summodc  11357  zsumdc  11358  fsum3  11361  isumz  11363  isumss  11365  fisumss  11366  isumss2  11367  fsum3cvg2  11368  fsumsersdc  11369  fsum3ser  11371  fsumsplit  11381  fsumsplitf  11382  isumlessdc  11470  prodfdivap  11521  cbvprod  11532  prodrbdclem  11545  prodmodclem2  11551  prodmodc  11552  zproddc  11553  fprodseq  11557  fprodntrivap  11558  prod1dc  11560  prodssdc  11563  fprodsplitdc  11570  fprod2dlemstep  11596  fproddivapf  11605  fprodsplitf  11606  suprzubdc  11918  nninfdcex  11919  zsupssdc  11920  nnmindc  12000  nnminle  12001  pcmptdvds  12308  nninfdclemcl  12414  nninfdclemp1  12416  ismnd  12684  sgrpidmndm  12685  dfgrp3me  12829  neipsm  13223  dedekindeulemub  13665  dedekindeulemloc  13666  dedekindeulemlub  13667  suplociccex  13672  dedekindicclemub  13674  dedekindicclemloc  13675  dedekindicclemlub  13676  limcimo  13703  lgsval  13974  lgsdir  14005  lgsdilem2  14006  lgsdi  14007  lgsne0  14008  2sqlem8  14028  bj-charfunbi  14121