Theorem eleq1w 2257

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

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

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548

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

This theorem is referenced by:  clelsb1f  2343  cbvralfw  2719  cbvrexfw  2720  cbvralvw  2733  cbvrexvw  2734  cbvreuvw  2735  dfdif3  3273  dfss4st  3396  abn0m  3476  r19.2m  3537  cbvmptf  4127  iinexgm  4187  xpiindim  4803  cnviinm  5211  iotam  5250  elfvm  5591  uchoice  6195  iinerm  6666  ixpiinm  6783  ixpsnf1o  6795  mapsnen  6870  pw2f1odclem  6895  enumctlemm  7180  nnnninfeq  7194  exmidomni  7208  fodjum  7212  exmidontriimlem4  7291  exmidontriim  7292  cc2  7334  suplocexprlemmu  7785  suplocsr  7876  axpre-suploc  7969  suprzubdc  10326  nninfdcex  10327  zsupssdc  10328  iseqf1olemqk  10599  seq3f1olemqsum  10605  summodclem2  11547  summodc  11548  zsumdc  11549  fsum3  11552  isumz  11554  isumss  11556  fisumss  11557  isumss2  11558  fsum3cvg2  11559  fsumsersdc  11560  fsum3ser  11562  fsumsplit  11572  fsumsplitf  11573  isumlessdc  11661  prodfdivap  11712  cbvprod  11723  prodrbdclem  11736  prodmodclem2  11742  prodmodc  11743  zproddc  11744  fprodseq  11748  fprodntrivap  11749  prod1dc  11751  prodssdc  11754  fprodsplitdc  11761  fprod2dlemstep  11787  fproddivapf  11796  fprodsplitf  11797  nnmindc  12201  nnminle  12202  nninfctlemfo  12207  pcmptdvds  12514  nninfdclemp1  12667  ismnd  13060  sgrpidmndm  13061  dfgrp3me  13232  issubg2m  13319  subrgintm  13799  islssm  13913  islidlm  14035  neipsm  14390  dedekindeulemub  14854  dedekindeulemloc  14855  dedekindeulemlub  14856  suplociccex  14861  dedekindicclemub  14863  dedekindicclemloc  14864  dedekindicclemlub  14865  limcimo  14901  dvmptfsum  14961  elply2  14971  lgsval  15245  lgsdir  15276  lgsdilem2  15277  lgsdi  15278  lgsne0  15279  lgsquadlem3  15320  lgsquad  15321  2sqlem8  15364  bj-charfunbi  15457