Theorem eleq1w 2257

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

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

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548

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

This theorem is referenced by:  clelsb1f  2343  cbvralfw  2719  cbvrexfw  2720  cbvralvw  2733  cbvrexvw  2734  cbvreuvw  2735  dfdif3  3274  dfss4st  3397  abn0m  3477  r19.2m  3538  cbvmptf  4128  iinexgm  4188  xpiindim  4804  cnviinm  5212  iotam  5251  elfvm  5594  uchoice  6204  iinerm  6675  ixpiinm  6792  ixpsnf1o  6804  mapsnen  6879  pw2f1odclem  6904  enumctlemm  7189  nnnninfeq  7203  exmidomni  7217  fodjum  7221  finacn  7289  exmidontriimlem4  7309  exmidontriim  7310  cc2  7352  suplocexprlemmu  7804  suplocsr  7895  axpre-suploc  7988  suprzubdc  10345  nninfdcex  10346  zsupssdc  10347  iseqf1olemqk  10618  seq3f1olemqsum  10624  summodclem2  11566  summodc  11567  zsumdc  11568  fsum3  11571  isumz  11573  isumss  11575  fisumss  11576  isumss2  11577  fsum3cvg2  11578  fsumsersdc  11579  fsum3ser  11581  fsumsplit  11591  fsumsplitf  11592  isumlessdc  11680  prodfdivap  11731  cbvprod  11742  prodrbdclem  11755  prodmodclem2  11761  prodmodc  11762  zproddc  11763  fprodseq  11767  fprodntrivap  11768  prod1dc  11770  prodssdc  11773  fprodsplitdc  11780  fprod2dlemstep  11806  fproddivapf  11815  fprodsplitf  11816  nnmindc  12228  nnminle  12229  nninfctlemfo  12234  pcmptdvds  12541  nninfdclemp1  12694  ismnd  13123  sgrpidmndm  13124  dfgrp3me  13304  issubg2m  13397  subrgintm  13877  islssm  13991  islidlm  14113  neipsm  14498  dedekindeulemub  14962  dedekindeulemloc  14963  dedekindeulemlub  14964  suplociccex  14969  dedekindicclemub  14971  dedekindicclemloc  14972  dedekindicclemlub  14973  limcimo  15009  dvmptfsum  15069  elply2  15079  lgsval  15353  lgsdir  15384  lgsdilem2  15385  lgsdi  15386  lgsne0  15387  lgsquadlem3  15428  lgsquad  15429  2sqlem8  15472  bj-charfunbi  15565