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  3314  dfss4st  3437  abn0m  3517  r19.2m  3578  cbvmptf  4177  iinexgm  4237  xpiindim  4858  reldmm  4941  cnviinm  5269  iotam  5309  elfvm  5659  cbvriotavw  5964  uchoice  6281  iinerm  6752  ixpiinm  6869  ixpsnf1o  6881  mapsnen  6962  pw2f1odclem  6991  enumctlemm  7277  nnnninfeq  7291  exmidomni  7305  fodjum  7309  finacn  7382  exmidontriimlem4  7402  exmidontriim  7403  cc2  7449  suplocexprlemmu  7901  suplocsr  7992  axpre-suploc  8085  suprzubdc  10451  nninfdcex  10452  zsupssdc  10453  iseqf1olemqk  10724  seq3f1olemqsum  10730  reuccatpfxs1  11274  summodclem2  11888  summodc  11889  zsumdc  11890  fsum3  11893  isumz  11895  isumss  11897  fisumss  11898  isumss2  11899  fsum3cvg2  11900  fsumsersdc  11901  fsum3ser  11903  fsumsplit  11913  fsumsplitf  11914  isumlessdc  12002  prodfdivap  12053  cbvprod  12064  prodrbdclem  12077  prodmodclem2  12083  prodmodc  12084  zproddc  12085  fprodseq  12089  fprodntrivap  12090  prod1dc  12092  prodssdc  12095  fprodsplitdc  12102  fprod2dlemstep  12128  fproddivapf  12137  fprodsplitf  12138  nnmindc  12550  nnminle  12551  nninfctlemfo  12556  pcmptdvds  12863  nninfdclemp1  13016  ismnd  13447  sgrpidmndm  13448  dfgrp3me  13628  issubg2m  13721  subrgintm  14201  islssm  14315  islidlm  14437  neipsm  14822  dedekindeulemub  15286  dedekindeulemloc  15287  dedekindeulemlub  15288  suplociccex  15293  dedekindicclemub  15295  dedekindicclemloc  15296  dedekindicclemlub  15297  limcimo  15333  dvmptfsum  15393  elply2  15403  lgsval  15677  lgsdir  15708  lgsdilem2  15709  lgsdi  15710  lgsne0  15711  lgsquadlem3  15752  lgsquad  15753  2sqlem8  15796  bj-charfunbi  16132