Theorem eleq1w 2226

Description: Weaker version of eleq1 2228 (but more general than elequ1 2140) not depending on ax-ext 2147 nor df-cleq 2158. (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 1701	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 ↔ 𝑧 = 𝑦))
2	1	anbi1d 461	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑧 = 𝑥 ∧ 𝑧 ∈ 𝐴) ↔ (𝑧 = 𝑦 ∧ 𝑧 ∈ 𝐴)))
3	2	exbidv 1813	. 2 ⊢ (𝑥 = 𝑦 → (∃𝑧(𝑧 = 𝑥 ∧ 𝑧 ∈ 𝐴) ↔ ∃𝑧(𝑧 = 𝑦 ∧ 𝑧 ∈ 𝐴)))
4		df-clel 2161	. 2 ⊢ (𝑥 ∈ 𝐴 ↔ ∃𝑧(𝑧 = 𝑥 ∧ 𝑧 ∈ 𝐴))
5		df-clel 2161	. 2 ⊢ (𝑦 ∈ 𝐴 ↔ ∃𝑧(𝑧 = 𝑦 ∧ 𝑧 ∈ 𝐴))
6	3, 4, 5	3bitr4g 222	1 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104  ∃wex 1480   ∈ wcel 2136

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522

This theorem depends on definitions:  df-bi 116  df-clel 2161

This theorem is referenced by:  clelsb1f  2311  cbvralfw  2682  cbvrexfw  2683  cbvralvw  2695  cbvrexvw  2696  cbvreuvw  2697  dfdif3  3231  dfss4st  3354  abn0m  3433  r19.2m  3494  cbvmptf  4075  iinexgm  4132  xpiindim  4740  cnviinm  5144  iinerm  6569  ixpiinm  6686  ixpsnf1o  6698  mapsnen  6773  enumctlemm  7075  nnnninfeq  7088  exmidomni  7102  fodjum  7106  exmidontriimlem4  7176  exmidontriim  7177  cc2  7204  suplocexprlemmu  7655  suplocsr  7746  axpre-suploc  7839  iseqf1olemqk  10425  seq3f1olemqsum  10431  summodclem2  11319  summodc  11320  zsumdc  11321  fsum3  11324  isumz  11326  isumss  11328  fisumss  11329  isumss2  11330  fsum3cvg2  11331  fsumsersdc  11332  fsum3ser  11334  fsumsplit  11344  fsumsplitf  11345  isumlessdc  11433  prodfdivap  11484  cbvprod  11495  prodrbdclem  11508  prodmodclem2  11514  prodmodc  11515  zproddc  11516  fprodseq  11520  fprodntrivap  11521  prod1dc  11523  prodssdc  11526  fprodsplitdc  11533  fprod2dlemstep  11559  fproddivapf  11568  fprodsplitf  11569  suprzubdc  11881  nninfdcex  11882  zsupssdc  11883  nnmindc  11963  nnminle  11964  pcmptdvds  12271  nninfdclemcl  12377  nninfdclemp1  12379  neipsm  12754  dedekindeulemub  13196  dedekindeulemloc  13197  dedekindeulemlub  13198  suplociccex  13203  dedekindicclemub  13205  dedekindicclemloc  13206  dedekindicclemlub  13207  limcimo  13234  lgsval  13505  lgsdir  13536  lgsdilem2  13537  lgsdi  13538  lgsne0  13539  2sqlem8  13559  bj-charfunbi  13653