Theorem eleq1w 2266

Description: Weaker version of eleq1 2268 (but more general than elequ1 2180) not depending on ax-ext 2187 nor df-cleq 2198. (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 1736	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 ↔ 𝑧 = 𝑦))
2	1	anbi1d 465	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑧 = 𝑥 ∧ 𝑧 ∈ 𝐴) ↔ (𝑧 = 𝑦 ∧ 𝑧 ∈ 𝐴)))
3	2	exbidv 1848	. 2 ⊢ (𝑥 = 𝑦 → (∃𝑧(𝑧 = 𝑥 ∧ 𝑧 ∈ 𝐴) ↔ ∃𝑧(𝑧 = 𝑦 ∧ 𝑧 ∈ 𝐴)))
4		df-clel 2201	. 2 ⊢ (𝑥 ∈ 𝐴 ↔ ∃𝑧(𝑧 = 𝑥 ∧ 𝑧 ∈ 𝐴))
5		df-clel 2201	. 2 ⊢ (𝑦 ∈ 𝐴 ↔ ∃𝑧(𝑧 = 𝑦 ∧ 𝑧 ∈ 𝐴))
6	3, 4, 5	3bitr4g 223	1 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))

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

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557

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

This theorem is referenced by:  clelsb1f  2352  cbvralfw  2728  cbvrexfw  2729  cbvralvw  2742  cbvrexvw  2743  cbvreuvw  2744  dfdif3  3283  dfss4st  3406  abn0m  3486  r19.2m  3547  cbvmptf  4138  iinexgm  4198  xpiindim  4815  cnviinm  5224  iotam  5263  elfvm  5609  uchoice  6223  iinerm  6694  ixpiinm  6811  ixpsnf1o  6823  mapsnen  6903  pw2f1odclem  6931  enumctlemm  7216  nnnninfeq  7230  exmidomni  7244  fodjum  7248  finacn  7316  exmidontriimlem4  7336  exmidontriim  7337  cc2  7379  suplocexprlemmu  7831  suplocsr  7922  axpre-suploc  8015  suprzubdc  10379  nninfdcex  10380  zsupssdc  10381  iseqf1olemqk  10652  seq3f1olemqsum  10658  summodclem2  11693  summodc  11694  zsumdc  11695  fsum3  11698  isumz  11700  isumss  11702  fisumss  11703  isumss2  11704  fsum3cvg2  11705  fsumsersdc  11706  fsum3ser  11708  fsumsplit  11718  fsumsplitf  11719  isumlessdc  11807  prodfdivap  11858  cbvprod  11869  prodrbdclem  11882  prodmodclem2  11888  prodmodc  11889  zproddc  11890  fprodseq  11894  fprodntrivap  11895  prod1dc  11897  prodssdc  11900  fprodsplitdc  11907  fprod2dlemstep  11933  fproddivapf  11942  fprodsplitf  11943  nnmindc  12355  nnminle  12356  nninfctlemfo  12361  pcmptdvds  12668  nninfdclemp1  12821  ismnd  13251  sgrpidmndm  13252  dfgrp3me  13432  issubg2m  13525  subrgintm  14005  islssm  14119  islidlm  14241  neipsm  14626  dedekindeulemub  15090  dedekindeulemloc  15091  dedekindeulemlub  15092  suplociccex  15097  dedekindicclemub  15099  dedekindicclemloc  15100  dedekindicclemlub  15101  limcimo  15137  dvmptfsum  15197  elply2  15207  lgsval  15481  lgsdir  15512  lgsdilem2  15513  lgsdi  15514  lgsne0  15515  lgsquadlem3  15556  lgsquad  15557  2sqlem8  15600  bj-charfunbi  15747