Theorem eleq1w 2824

Description: Weaker version of eleq1 2829 (but more general than elequ1 2115) not depending on ax-ext 2708 nor df-cleq 2729.

Note that this provides a proof of ax-8 2110 from Tarski's FOL and dfclel 2817 (simply consider an instance where 𝐴 is replaced by a setvar and deduce the forward implication by biimpd 229), which shows that dfclel 2817 is too powerful to be used as a definition instead of df-clel 2816. (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 2025	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 ↔ 𝑧 = 𝑦))
2	1	anbi1d 631	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑧 = 𝑥 ∧ 𝑧 ∈ 𝐴) ↔ (𝑧 = 𝑦 ∧ 𝑧 ∈ 𝐴)))
3	2	exbidv 1921	. 2 ⊢ (𝑥 = 𝑦 → (∃𝑧(𝑧 = 𝑥 ∧ 𝑧 ∈ 𝐴) ↔ ∃𝑧(𝑧 = 𝑦 ∧ 𝑧 ∈ 𝐴)))
4		dfclel 2817	. 2 ⊢ (𝑥 ∈ 𝐴 ↔ ∃𝑧(𝑧 = 𝑥 ∧ 𝑧 ∈ 𝐴))
5		dfclel 2817	. 2 ⊢ (𝑦 ∈ 𝐴 ↔ ∃𝑧(𝑧 = 𝑦 ∧ 𝑧 ∈ 𝐴))
6	3, 4, 5	3bitr4g 314	1 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∃wex 1779   ∈ wcel 2108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-clel 2816

This theorem is referenced by:  clelsb1  2868  cleqh  2871  nfcjust  2891  nfcr  2895  cleqf  2934  rspw  3236  cbvralvw  3237  cbvrexvw  3238  cbvralfw  3304  cbvralsvw  3317  cbvralf  3360  ralcom2  3377  moel  3402  cbvrmovw  3403  cbvreuvw  3404  moelOLD  3405  cbvrmow  3409  cbvreuwOLD  3415  cbvreu  3428  cbvrabv  3447  rabrabi  3456  cbvrabw  3473  cbvrabwOLD  3474  nfrab  3478  cbvrab  3479  elrab2w  3696  reu2  3731  reu6  3732  rmo4  3736  reu8  3739  2reu5  3764  ruOLD  3787  csbied  3935  difjust  3953  unjust  3955  injust  3957  dfss2  3969  dfssf  3974  dfdif3OLD  4118  eqeuel  4365  rabeq0w  4387  disj  4450  reldisj  4453  ralidmw  4508  dfif6  4528  rabsnifsb  4722  eluniab  4921  unissb  4939  elintabOLD  4959  uniintsn  4985  dfiun2g  5030  dfiunv2  5035  disjxun  5141  cbvmptf  5251  cbvmptfg  5252  cbvmptv  5255  dftr2c  5262  isso2i  5629  dfres2  6059  imai  6092  frpoinsg  6364  wfisgOLD  6375  tz7.7  6410  fvn0ssdmfun  7094  fmptco  7149  cbvriotaw  7397  cbvriotavw  7398  cbvriota  7401  cbvmpox  7526  cbvmpov  7528  tfis  7876  tfindes  7884  peano5  7915  findes  7922  dfoprab4f  8081  fmpox  8092  xpord2indlem  8172  poseq  8183  soseq  8184  wfrlem10OLD  8358  smogt  8407  resixpfo  8976  ixpsnf1o  8978  dom2lem  9032  mapsnend  9076  pw2f1olem  9116  pssnn  9208  ssfi  9213  findcard3  9318  findcard3OLD  9319  ordiso2  9555  elirrv  9636  cantnflem1d  9728  cantnf  9733  setind  9774  frinsg  9791  tz9.12lem3  9829  infxpen  10054  dfac5lem4  10166  dfac12lem2  10185  kmlem14  10204  cfsmolem  10310  sornom  10317  isf32lem9  10401  axdc2  10489  fpwwe2lem7  10677  fpwwe2  10683  wunex2  10778  dedekindle  11425  wloglei  11795  uzind4s  12950  seqof2  14101  reuccatpfxs1  14785  shftfn  15112  rexuz3  15387  zsum  15754  fsum  15756  sumss  15760  sumss2  15762  fsumcvg2  15763  fsumser  15766  fsumclf  15774  fsumsplitf  15778  isumless  15881  prodfdiv  15932  cbvprod  15949  cbvprodv  15950  zprod  15973  fprod  15977  fprodntriv  15978  prodss  15983  fprod2dlem  16016  fproddivf  16023  fprodsplitf  16024  rpnnen2lem10  16259  cpnnen  16265  sumeven  16424  sumodd  16425  sadcp1  16492  smupp1  16517  pcmptdvds  16932  prmreclem2  16955  prmreclem5  16958  prmreclem6  16959  prmrec  16960  prmdvdsprmo  17080  iscatd2  17724  initoeu2  18061  yoniso  18330  sgrpidmnd  18752  mndind  18841  eqg0subg  19214  symggen  19488  dprd2d2  20064  srhmsubc  20680  isdrngrd  20766  isdrngrdOLD  20768  lbspss  21081  frlmphl  21801  frlmup1  21818  opsrtoslem1  22079  mdetralt  22614  mdetralt2  22615  mdetunilem2  22619  maducoeval2  22646  chfacfscmulgsum  22866  chfacfpmmulgsum  22870  isclo2  23096  neiptopnei  23140  ptcldmpt  23622  elmptrab  23835  hausflimi  23988  hausflim  23989  alexsubALTlem3  24057  alexsubALTlem4  24058  ptcmplem2  24061  cnextcn  24075  cnextfres1  24076  tgphaus  24125  ustuqtop  24255  utopsnneip  24257  ucncn  24294  nrmmetd  24587  xrhmeo  24977  iscau2  25311  caucfil  25317  cmetcaulem  25322  bcth  25363  vitalilem3  25645  vitali  25648  i1f1lem  25724  itg11  25726  i1fres  25740  mbfi1fseq  25756  mbfi1flim  25758  itg2uba  25778  itg2splitlem  25783  isibl2  25801  cbvitg  25811  cbvitgv  25812  itgss3  25850  dvmptfsum  26013  rolle  26028  elply2  26235  plyexmo  26355  lgamgulmlem2  27073  prmorcht  27221  pclogsum  27259  dchr1  27301  lgsdir  27376  lgsdilem2  27377  lgsdi  27378  lgsne0  27379  lgsquadlem3  27426  lgsquad  27427  2sqlem8  27470  nosupcbv  27747  nosupno  27748  nosupdm  27749  nosupbnd1lem1  27753  noinfcbv  27762  noinfno  27763  noinfdm  27764  nocvxminlem  27822  legval  28592  legov  28593  tglineintmo  28650  tglowdim2ln  28659  ishpg  28767  lnopp2hpgb  28771  hpgerlem  28773  colopp  28777  axcontlem1  28979  numedglnl  29161  uvtxnbgrvtx  29410  cusgrres  29466  wspniunwspnon  29943  rusgrnumwwlkb0  29991  frgr3vlem2  30293  3vfriswmgrlem  30296  fusgr2wsp2nb  30353  numclwlk2lem2f1o  30398  lpni  30499  pjhthmo  31321  chscllem2  31657  cbvdisjf  32584  2ndresdju  32659  fmptcof2  32667  aciunf1lem  32672  funcnv4mpt  32679  suppovss  32690  fpwrelmapffslem  32743  fsumiunle  32831  gsumwrd2dccatlem  33069  elrspunsn  33457  1arithufdlem3  33574  fedgmullem1  33680  fldextrspunlsp  33724  zarclssn  33872  esumcvg  34087  fiunelros  34175  measiun  34219  bnj1146  34805  bnj1185  34807  bnj1385  34846  bnj1014  34975  bnj1112  34997  bnj1123  35000  bnj1228  35025  bnj1326  35040  bnj1321  35041  bnj1384  35046  bnj1417  35055  bnj1497  35074  gonarlem  35399  goalrlem  35401  goalr  35402  mrsubrn  35518  dfon2lem6  35789  dfbigcup2  35900  lineintmo  36158  cbvralvw2  36227  cbvrexvw2  36228  cbvrmovw2  36229  cbvreuvw2  36230  cbvmptvw2  36235  cbvprodvw2  36248  cbvrmodavw  36253  cbvreudavw  36254  cbvrabdavw  36262  cbvmptdavw  36268  cbvriotadavw  36271  cbvixpdavw  36279  cbvproddavw  36281  cbvitgdavw  36282  cbvrabdavw2  36286  cbvmptdavw2  36289  cbvriotadavw2  36291  weiunlem2  36464  eleq2w2ALT  37048  bj-idres  37161  mptsnunlem  37339  ptrest  37626  poimirlem25  37652  mblfinlem2  37665  mblfinlem3  37666  mblfinlem4  37667  ismblfin  37668  mbfposadd  37674  itg2addnclem  37678  ftc1anclem5  37704  ftc1anclem6  37705  ftc1anclem7  37706  ftc1anc  37708  areacirclem5  37719  fdc1  37753  inxprnres  38293  fsumshftd  38953  pmapglb  39772  polval2N  39908  osumcllem4N  39961  pexmidlem1N  39972  dih1dimatlem  41331  mapdh9a  41791  mapdh9aOLDN  41792  sticksstones2  42148  selvvvval  42595  fsuppind  42600  fphpd  42827  fphpdo  42828  pellex  42846  setindtrs  43037  dford3lem2  43039  fnwe2lem2  43063  mendlmod  43201  cantnfub  43334  tfsconcat0i  43358  rababg  43587  fsovrfovd  44022  fsovcnvlem  44026  scottabf  44259  trfr  44979  elunif  45021  iunincfi  45099  cbvmpo2  45102  cbvmpo1  45103  disjf1  45188  wessf1ornlem  45190  disjinfi  45197  supxrleubrnmptf  45462  monoordxr  45493  monoord2xr  45495  fsummulc1f  45586  fsumnncl  45587  fsumf1of  45589  fsumiunss  45590  fsumreclf  45591  fsumlessf  45592  fsumsermpt  45594  fmulcl  45596  fmul01lt1lem2  45600  fprodexp  45609  fprodabs2  45610  climmulf  45619  climexp  45620  climrecf  45624  climinff  45626  climaddf  45630  mullimc  45631  limcperiod  45643  sumnnodd  45645  neglimc  45662  addlimc  45663  climsubmpt  45675  climreclf  45679  climeldmeqmpt  45683  climfveqmpt  45686  fnlimfvre  45689  climfveqf  45695  climfveqmpt3  45697  climeldmeqf  45698  climeqf  45703  climeldmeqmpt3  45704  climinf2  45722  limsupequz  45738  limsupequzmptf  45746  lmbr3  45762  cnrefiisp  45845  cncfshift  45889  fprodcncf  45915  dvmptmulf  45952  dvmptfprod  45960  dvnprodlem1  45961  dvnprodlem3  45963  stoweidlem16  46031  stoweidlem34  46049  stoweidlem62  46077  dirkercncflem2  46119  fourierdlem12  46134  fourierdlem15  46137  fourierdlem34  46156  fourierdlem50  46171  fourierdlem73  46194  fourierdlem94  46215  fourierdlem112  46233  fourierdlem113  46234  intsaluni  46344  sge0lempt  46425  sge0iunmptlemfi  46428  sge0iunmptlemre  46430  sge0iunmpt  46433  sge0ltfirpmpt2  46441  sge0isummpt2  46447  sge0xaddlem2  46449  sge0xadd  46450  meadjiun  46481  voliunsge0lem  46487  meaiuninclem  46495  meaiunincf  46498  meaiuninc3v  46499  meaiuninc3  46500  meaiininclem  46501  meaiininc  46502  isomennd  46546  ovn0lem  46580  sge0hsphoire  46604  hoidmvlelem1  46610  hoidmvlelem2  46611  hoidmvlelem3  46612  hoidmvlelem5  46614  hspmbllem2  46642  hoimbl2  46680  vonhoire  46687  vonioo  46697  vonicc  46700  vonn0ioo2  46705  vonn0icc2  46707  pimincfltioc  46731  salpreimagtlt  46745  smflimlem4  46789  ormkglobd  46890  rexrsb  47112  ichexmpl2  47457  ichnreuop  47459  sbgoldbm  47771  bgoldbnnsum3prm  47791  tgoldbach  47804  srhmsubcALTV  48241  cbvmpox2  48252  mo0sn  48735  f1omo  48792  isthincd2lem1  49075  thincmo  49077