Theorem eleq1w 2254

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

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

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545

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

This theorem is referenced by:  clelsb1f  2340  cbvralfw  2716  cbvrexfw  2717  cbvralvw  2730  cbvrexvw  2731  cbvreuvw  2732  dfdif3  3270  dfss4st  3393  abn0m  3473  r19.2m  3534  cbvmptf  4124  iinexgm  4184  xpiindim  4800  cnviinm  5208  iotam  5247  elfvm  5588  uchoice  6192  iinerm  6663  ixpiinm  6780  ixpsnf1o  6792  mapsnen  6867  pw2f1odclem  6892  enumctlemm  7175  nnnninfeq  7189  exmidomni  7203  fodjum  7207  exmidontriimlem4  7286  exmidontriim  7287  cc2  7329  suplocexprlemmu  7780  suplocsr  7871  axpre-suploc  7964  iseqf1olemqk  10581  seq3f1olemqsum  10587  summodclem2  11528  summodc  11529  zsumdc  11530  fsum3  11533  isumz  11535  isumss  11537  fisumss  11538  isumss2  11539  fsum3cvg2  11540  fsumsersdc  11541  fsum3ser  11543  fsumsplit  11553  fsumsplitf  11554  isumlessdc  11642  prodfdivap  11693  cbvprod  11704  prodrbdclem  11717  prodmodclem2  11723  prodmodc  11724  zproddc  11725  fprodseq  11729  fprodntrivap  11730  prod1dc  11732  prodssdc  11735  fprodsplitdc  11742  fprod2dlemstep  11768  fproddivapf  11777  fprodsplitf  11778  suprzubdc  12092  nninfdcex  12093  zsupssdc  12094  nnmindc  12174  nnminle  12175  nninfctlemfo  12180  pcmptdvds  12486  nninfdclemp1  12610  ismnd  13003  sgrpidmndm  13004  dfgrp3me  13175  issubg2m  13262  subrgintm  13742  islssm  13856  islidlm  13978  neipsm  14333  dedekindeulemub  14797  dedekindeulemloc  14798  dedekindeulemlub  14799  suplociccex  14804  dedekindicclemub  14806  dedekindicclemloc  14807  dedekindicclemlub  14808  limcimo  14844  dvmptfsum  14904  elply2  14914  lgsval  15161  lgsdir  15192  lgsdilem2  15193  lgsdi  15194  lgsne0  15195  lgsquadlem3  15236  lgsquad  15237  2sqlem8  15280  bj-charfunbi  15373