Theorem eleq1w 2231

Description: Weaker version of eleq1 2233 (but more general than elequ1 2145) not depending on ax-ext 2152 nor df-cleq 2163. (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 1706	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 ↔ 𝑧 = 𝑦))
2	1	anbi1d 462	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑧 = 𝑥 ∧ 𝑧 ∈ 𝐴) ↔ (𝑧 = 𝑦 ∧ 𝑧 ∈ 𝐴)))
3	2	exbidv 1818	. 2 ⊢ (𝑥 = 𝑦 → (∃𝑧(𝑧 = 𝑥 ∧ 𝑧 ∈ 𝐴) ↔ ∃𝑧(𝑧 = 𝑦 ∧ 𝑧 ∈ 𝐴)))
4		df-clel 2166	. 2 ⊢ (𝑥 ∈ 𝐴 ↔ ∃𝑧(𝑧 = 𝑥 ∧ 𝑧 ∈ 𝐴))
5		df-clel 2166	. 2 ⊢ (𝑦 ∈ 𝐴 ↔ ∃𝑧(𝑧 = 𝑦 ∧ 𝑧 ∈ 𝐴))
6	3, 4, 5	3bitr4g 222	1 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))

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

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 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527

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

This theorem is referenced by:  clelsb1f  2316  cbvralfw  2687  cbvrexfw  2688  cbvralvw  2700  cbvrexvw  2701  cbvreuvw  2702  dfdif3  3237  dfss4st  3360  abn0m  3440  r19.2m  3501  cbvmptf  4083  iinexgm  4140  xpiindim  4748  cnviinm  5152  iotam  5190  iinerm  6585  ixpiinm  6702  ixpsnf1o  6714  mapsnen  6789  enumctlemm  7091  nnnninfeq  7104  exmidomni  7118  fodjum  7122  exmidontriimlem4  7201  exmidontriim  7202  cc2  7229  suplocexprlemmu  7680  suplocsr  7771  axpre-suploc  7864  iseqf1olemqk  10450  seq3f1olemqsum  10456  summodclem2  11345  summodc  11346  zsumdc  11347  fsum3  11350  isumz  11352  isumss  11354  fisumss  11355  isumss2  11356  fsum3cvg2  11357  fsumsersdc  11358  fsum3ser  11360  fsumsplit  11370  fsumsplitf  11371  isumlessdc  11459  prodfdivap  11510  cbvprod  11521  prodrbdclem  11534  prodmodclem2  11540  prodmodc  11541  zproddc  11542  fprodseq  11546  fprodntrivap  11547  prod1dc  11549  prodssdc  11552  fprodsplitdc  11559  fprod2dlemstep  11585  fproddivapf  11594  fprodsplitf  11595  suprzubdc  11907  nninfdcex  11908  zsupssdc  11909  nnmindc  11989  nnminle  11990  pcmptdvds  12297  nninfdclemcl  12403  nninfdclemp1  12405  ismnd  12655  sgrpidmndm  12656  neipsm  12948  dedekindeulemub  13390  dedekindeulemloc  13391  dedekindeulemlub  13392  suplociccex  13397  dedekindicclemub  13399  dedekindicclemloc  13400  dedekindicclemlub  13401  limcimo  13428  lgsval  13699  lgsdir  13730  lgsdilem2  13731  lgsdi  13732  lgsne0  13733  2sqlem8  13753  bj-charfunbi  13846