Theorem eleq1w 2250

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

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

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545

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

This theorem is referenced by:  clelsb1f  2336  cbvralfw  2708  cbvrexfw  2709  cbvralvw  2722  cbvrexvw  2723  cbvreuvw  2724  dfdif3  3260  dfss4st  3383  abn0m  3463  r19.2m  3524  cbvmptf  4112  iinexgm  4172  xpiindim  4782  cnviinm  5188  iotam  5227  elfvm  5567  iinerm  6634  ixpiinm  6751  ixpsnf1o  6763  mapsnen  6838  pw2f1odclem  6863  enumctlemm  7144  nnnninfeq  7157  exmidomni  7171  fodjum  7175  exmidontriimlem4  7254  exmidontriim  7255  cc2  7297  suplocexprlemmu  7748  suplocsr  7839  axpre-suploc  7932  iseqf1olemqk  10527  seq3f1olemqsum  10533  summodclem2  11425  summodc  11426  zsumdc  11427  fsum3  11430  isumz  11432  isumss  11434  fisumss  11435  isumss2  11436  fsum3cvg2  11437  fsumsersdc  11438  fsum3ser  11440  fsumsplit  11450  fsumsplitf  11451  isumlessdc  11539  prodfdivap  11590  cbvprod  11601  prodrbdclem  11614  prodmodclem2  11620  prodmodc  11621  zproddc  11622  fprodseq  11626  fprodntrivap  11627  prod1dc  11629  prodssdc  11632  fprodsplitdc  11639  fprod2dlemstep  11665  fproddivapf  11674  fprodsplitf  11675  suprzubdc  11988  nninfdcex  11989  zsupssdc  11990  nnmindc  12070  nnminle  12071  pcmptdvds  12380  nninfdclemp1  12504  ismnd  12895  sgrpidmndm  12896  dfgrp3me  13059  issubg2m  13145  subrgintm  13607  islssm  13690  islidlm  13812  neipsm  14131  dedekindeulemub  14573  dedekindeulemloc  14574  dedekindeulemlub  14575  suplociccex  14580  dedekindicclemub  14582  dedekindicclemloc  14583  dedekindicclemlub  14584  limcimo  14611  lgsval  14883  lgsdir  14914  lgsdilem2  14915  lgsdi  14916  lgsne0  14917  2sqlem8  14948  bj-charfunbi  15041