Theorem eleq1w 2290

Description: Weaker version of eleq1 2292 (but more general than elequ1 2204) not depending on ax-ext 2211 nor df-cleq 2222. (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 1759	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 ↔ 𝑧 = 𝑦))
2	1	anbi1d 465	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑧 = 𝑥 ∧ 𝑧 ∈ 𝐴) ↔ (𝑧 = 𝑦 ∧ 𝑧 ∈ 𝐴)))
3	2	exbidv 1871	. 2 ⊢ (𝑥 = 𝑦 → (∃𝑧(𝑧 = 𝑥 ∧ 𝑧 ∈ 𝐴) ↔ ∃𝑧(𝑧 = 𝑦 ∧ 𝑧 ∈ 𝐴)))
4		df-clel 2225	. 2 ⊢ (𝑥 ∈ 𝐴 ↔ ∃𝑧(𝑧 = 𝑥 ∧ 𝑧 ∈ 𝐴))
5		df-clel 2225	. 2 ⊢ (𝑦 ∈ 𝐴 ↔ ∃𝑧(𝑧 = 𝑦 ∧ 𝑧 ∈ 𝐴))
6	3, 4, 5	3bitr4g 223	1 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))

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

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580

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

This theorem is referenced by:  clelsb1f  2376  cbvrmow  2714  cbvralfw  2754  cbvrexfw  2755  cbvralvw  2769  cbvrexvw  2770  cbvreuvw  2771  dfdif3  3315  dfss4st  3438  abn0m  3518  r19.2m  3579  rabsnifsb  3735  cbvmptf  4181  iinexgm  4242  xpiindim  4865  reldmm  4948  cnviinm  5276  iotam  5316  elfvm  5668  cbvriotavw  5977  uchoice  6295  iinerm  6771  ixpiinm  6888  ixpsnf1o  6900  mapsnen  6981  pw2f1odclem  7015  enumctlemm  7304  nnnninfeq  7318  exmidomni  7332  fodjum  7336  finacn  7409  exmidontriimlem4  7429  exmidontriim  7430  cc2  7476  suplocexprlemmu  7928  suplocsr  8019  axpre-suploc  8112  suprzubdc  10486  nninfdcex  10487  zsupssdc  10488  iseqf1olemqk  10759  seq3f1olemqsum  10765  reuccatpfxs1  11318  summodclem2  11933  summodc  11934  zsumdc  11935  fsum3  11938  isumz  11940  isumss  11942  fisumss  11943  isumss2  11944  fsum3cvg2  11945  fsumsersdc  11946  fsum3ser  11948  fsumsplit  11958  fsumsplitf  11959  isumlessdc  12047  prodfdivap  12098  cbvprod  12109  prodrbdclem  12122  prodmodclem2  12128  prodmodc  12129  zproddc  12130  fprodseq  12134  fprodntrivap  12135  prod1dc  12137  prodssdc  12140  fprodsplitdc  12147  fprod2dlemstep  12173  fproddivapf  12182  fprodsplitf  12183  nnmindc  12595  nnminle  12596  nninfctlemfo  12601  pcmptdvds  12908  nninfdclemp1  13061  ismnd  13492  sgrpidmndm  13493  dfgrp3me  13673  issubg2m  13766  subrgintm  14247  islssm  14361  islidlm  14483  neipsm  14868  dedekindeulemub  15332  dedekindeulemloc  15333  dedekindeulemlub  15334  suplociccex  15339  dedekindicclemub  15341  dedekindicclemloc  15342  dedekindicclemlub  15343  limcimo  15379  dvmptfsum  15439  elply2  15449  lgsval  15723  lgsdir  15754  lgsdilem2  15755  lgsdi  15756  lgsne0  15757  lgsquadlem3  15798  lgsquad  15799  2sqlem8  15842  bj-charfunbi  16342