Theorem eleq1w 2265

Description: Weaker version of eleq1 2267 (but more general than elequ1 2179) not depending on ax-ext 2186 nor df-cleq 2197. (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 1735	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 ↔ 𝑧 = 𝑦))
2	1	anbi1d 465	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑧 = 𝑥 ∧ 𝑧 ∈ 𝐴) ↔ (𝑧 = 𝑦 ∧ 𝑧 ∈ 𝐴)))
3	2	exbidv 1847	. 2 ⊢ (𝑥 = 𝑦 → (∃𝑧(𝑧 = 𝑥 ∧ 𝑧 ∈ 𝐴) ↔ ∃𝑧(𝑧 = 𝑦 ∧ 𝑧 ∈ 𝐴)))
4		df-clel 2200	. 2 ⊢ (𝑥 ∈ 𝐴 ↔ ∃𝑧(𝑧 = 𝑥 ∧ 𝑧 ∈ 𝐴))
5		df-clel 2200	. 2 ⊢ (𝑦 ∈ 𝐴 ↔ ∃𝑧(𝑧 = 𝑦 ∧ 𝑧 ∈ 𝐴))
6	3, 4, 5	3bitr4g 223	1 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))

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

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 1469  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556

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

This theorem is referenced by:  clelsb1f  2351  cbvralfw  2727  cbvrexfw  2728  cbvralvw  2741  cbvrexvw  2742  cbvreuvw  2743  dfdif3  3282  dfss4st  3405  abn0m  3485  r19.2m  3546  cbvmptf  4137  iinexgm  4197  xpiindim  4814  cnviinm  5223  iotam  5262  elfvm  5608  uchoice  6222  iinerm  6693  ixpiinm  6810  ixpsnf1o  6822  mapsnen  6902  pw2f1odclem  6930  enumctlemm  7215  nnnninfeq  7229  exmidomni  7243  fodjum  7247  finacn  7315  exmidontriimlem4  7335  exmidontriim  7336  cc2  7378  suplocexprlemmu  7830  suplocsr  7921  axpre-suploc  8014  suprzubdc  10377  nninfdcex  10378  zsupssdc  10379  iseqf1olemqk  10650  seq3f1olemqsum  10656  summodclem2  11635  summodc  11636  zsumdc  11637  fsum3  11640  isumz  11642  isumss  11644  fisumss  11645  isumss2  11646  fsum3cvg2  11647  fsumsersdc  11648  fsum3ser  11650  fsumsplit  11660  fsumsplitf  11661  isumlessdc  11749  prodfdivap  11800  cbvprod  11811  prodrbdclem  11824  prodmodclem2  11830  prodmodc  11831  zproddc  11832  fprodseq  11836  fprodntrivap  11837  prod1dc  11839  prodssdc  11842  fprodsplitdc  11849  fprod2dlemstep  11875  fproddivapf  11884  fprodsplitf  11885  nnmindc  12297  nnminle  12298  nninfctlemfo  12303  pcmptdvds  12610  nninfdclemp1  12763  ismnd  13193  sgrpidmndm  13194  dfgrp3me  13374  issubg2m  13467  subrgintm  13947  islssm  14061  islidlm  14183  neipsm  14568  dedekindeulemub  15032  dedekindeulemloc  15033  dedekindeulemlub  15034  suplociccex  15039  dedekindicclemub  15041  dedekindicclemloc  15042  dedekindicclemlub  15043  limcimo  15079  dvmptfsum  15139  elply2  15149  lgsval  15423  lgsdir  15454  lgsdilem2  15455  lgsdi  15456  lgsne0  15457  lgsquadlem3  15498  lgsquad  15499  2sqlem8  15542  bj-charfunbi  15680