Theorem eleq1w 2238

Description: Weaker version of eleq1 2240 (but more general than elequ1 2152) not depending on ax-ext 2159 nor df-cleq 2170. (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 1713	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 ↔ 𝑧 = 𝑦))
2	1	anbi1d 465	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑧 = 𝑥 ∧ 𝑧 ∈ 𝐴) ↔ (𝑧 = 𝑦 ∧ 𝑧 ∈ 𝐴)))
3	2	exbidv 1825	. 2 ⊢ (𝑥 = 𝑦 → (∃𝑧(𝑧 = 𝑥 ∧ 𝑧 ∈ 𝐴) ↔ ∃𝑧(𝑧 = 𝑦 ∧ 𝑧 ∈ 𝐴)))
4		df-clel 2173	. 2 ⊢ (𝑥 ∈ 𝐴 ↔ ∃𝑧(𝑧 = 𝑥 ∧ 𝑧 ∈ 𝐴))
5		df-clel 2173	. 2 ⊢ (𝑦 ∈ 𝐴 ↔ ∃𝑧(𝑧 = 𝑦 ∧ 𝑧 ∈ 𝐴))
6	3, 4, 5	3bitr4g 223	1 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))

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

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534

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

This theorem is referenced by:  clelsb1f  2323  cbvralfw  2695  cbvrexfw  2696  cbvralvw  2708  cbvrexvw  2709  cbvreuvw  2710  dfdif3  3246  dfss4st  3369  abn0m  3449  r19.2m  3510  cbvmptf  4098  iinexgm  4155  xpiindim  4765  cnviinm  5171  iotam  5209  iinerm  6607  ixpiinm  6724  ixpsnf1o  6736  mapsnen  6811  enumctlemm  7113  nnnninfeq  7126  exmidomni  7140  fodjum  7144  exmidontriimlem4  7223  exmidontriim  7224  cc2  7266  suplocexprlemmu  7717  suplocsr  7808  axpre-suploc  7901  iseqf1olemqk  10494  seq3f1olemqsum  10500  summodclem2  11390  summodc  11391  zsumdc  11392  fsum3  11395  isumz  11397  isumss  11399  fisumss  11400  isumss2  11401  fsum3cvg2  11402  fsumsersdc  11403  fsum3ser  11405  fsumsplit  11415  fsumsplitf  11416  isumlessdc  11504  prodfdivap  11555  cbvprod  11566  prodrbdclem  11579  prodmodclem2  11585  prodmodc  11586  zproddc  11587  fprodseq  11591  fprodntrivap  11592  prod1dc  11594  prodssdc  11597  fprodsplitdc  11604  fprod2dlemstep  11630  fproddivapf  11639  fprodsplitf  11640  suprzubdc  11953  nninfdcex  11954  zsupssdc  11955  nnmindc  12035  nnminle  12036  pcmptdvds  12343  nninfdclemcl  12449  nninfdclemp1  12451  ismnd  12820  sgrpidmndm  12821  dfgrp3me  12970  issubg2m  13049  subrgintm  13364  neipsm  13657  dedekindeulemub  14099  dedekindeulemloc  14100  dedekindeulemlub  14101  suplociccex  14106  dedekindicclemub  14108  dedekindicclemloc  14109  dedekindicclemlub  14110  limcimo  14137  lgsval  14408  lgsdir  14439  lgsdilem2  14440  lgsdi  14441  lgsne0  14442  2sqlem8  14473  bj-charfunbi  14566