Theorem eleq1w 2267

Description: Weaker version of eleq1 2269 (but more general than elequ1 2181) not depending on ax-ext 2188 nor df-cleq 2199. (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 1737	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 ↔ 𝑧 = 𝑦))
2	1	anbi1d 465	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑧 = 𝑥 ∧ 𝑧 ∈ 𝐴) ↔ (𝑧 = 𝑦 ∧ 𝑧 ∈ 𝐴)))
3	2	exbidv 1849	. 2 ⊢ (𝑥 = 𝑦 → (∃𝑧(𝑧 = 𝑥 ∧ 𝑧 ∈ 𝐴) ↔ ∃𝑧(𝑧 = 𝑦 ∧ 𝑧 ∈ 𝐴)))
4		df-clel 2202	. 2 ⊢ (𝑥 ∈ 𝐴 ↔ ∃𝑧(𝑧 = 𝑥 ∧ 𝑧 ∈ 𝐴))
5		df-clel 2202	. 2 ⊢ (𝑦 ∈ 𝐴 ↔ ∃𝑧(𝑧 = 𝑦 ∧ 𝑧 ∈ 𝐴))
6	3, 4, 5	3bitr4g 223	1 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))

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

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558

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

This theorem is referenced by:  clelsb1f  2353  cbvralfw  2729  cbvrexfw  2730  cbvralvw  2743  cbvrexvw  2744  cbvreuvw  2745  dfdif3  3287  dfss4st  3410  abn0m  3490  r19.2m  3551  cbvmptf  4149  iinexgm  4209  xpiindim  4828  cnviinm  5238  iotam  5277  elfvm  5627  uchoice  6241  iinerm  6712  ixpiinm  6829  ixpsnf1o  6841  mapsnen  6922  pw2f1odclem  6951  enumctlemm  7237  nnnninfeq  7251  exmidomni  7265  fodjum  7269  finacn  7342  exmidontriimlem4  7362  exmidontriim  7363  cc2  7409  suplocexprlemmu  7861  suplocsr  7952  axpre-suploc  8045  suprzubdc  10411  nninfdcex  10412  zsupssdc  10413  iseqf1olemqk  10684  seq3f1olemqsum  10690  summodclem2  11778  summodc  11779  zsumdc  11780  fsum3  11783  isumz  11785  isumss  11787  fisumss  11788  isumss2  11789  fsum3cvg2  11790  fsumsersdc  11791  fsum3ser  11793  fsumsplit  11803  fsumsplitf  11804  isumlessdc  11892  prodfdivap  11943  cbvprod  11954  prodrbdclem  11967  prodmodclem2  11973  prodmodc  11974  zproddc  11975  fprodseq  11979  fprodntrivap  11980  prod1dc  11982  prodssdc  11985  fprodsplitdc  11992  fprod2dlemstep  12018  fproddivapf  12027  fprodsplitf  12028  nnmindc  12440  nnminle  12441  nninfctlemfo  12446  pcmptdvds  12753  nninfdclemp1  12906  ismnd  13336  sgrpidmndm  13337  dfgrp3me  13517  issubg2m  13610  subrgintm  14090  islssm  14204  islidlm  14326  neipsm  14711  dedekindeulemub  15175  dedekindeulemloc  15176  dedekindeulemlub  15177  suplociccex  15182  dedekindicclemub  15184  dedekindicclemloc  15185  dedekindicclemlub  15186  limcimo  15222  dvmptfsum  15282  elply2  15292  lgsval  15566  lgsdir  15597  lgsdilem2  15598  lgsdi  15599  lgsne0  15600  lgsquadlem3  15641  lgsquad  15642  2sqlem8  15685  bj-charfunbi  15916