Theorem eleq1w 2819

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

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-clel 2811

This theorem is referenced by:  clelsb1  2863  cleqh  2865  nfcjust  2884  nfcr  2888  cleqf  2927  rspw  3213  cbvralvw  3214  cbvrexvw  3215  cbvralfw  3276  cbvralsvw  3287  cbvralf  3330  ralcom2  3347  moel  3370  cbvrmovw  3371  cbvreuvw  3372  cbvrmow  3375  cbvreu  3391  cbvrabv  3409  rabrabi  3418  cbvrabw  3434  cbvrabwOLD  3435  nfrab  3438  cbvrab  3439  elrab2w  3650  reu2  3683  reu6  3684  rmo4  3688  reu8  3691  2reu5  3716  ruOLD  3739  csbied  3885  difjust  3903  unjust  3905  injust  3907  dfss2  3919  dfssf  3924  dfdif3OLD  4070  eqeuel  4317  rabeq0w  4339  disj  4402  reldisj  4405  ralidmw  4469  dfif6  4482  rabsnifsb  4679  eluniab  4877  unissb  4896  uniintsn  4940  dfiun2g  4985  dfiunv2  4989  disjxun  5096  cbvmptf  5198  cbvmptfg  5199  cbvmptv  5202  dftr2c  5208  isso2i  5569  dfres2  6000  imai  6033  frpoinsg  6301  tz7.7  6343  fvn0ssdmfun  7019  fmptco  7074  cbvriotaw  7324  cbvriotavw  7325  cbvriota  7328  cbvmpox  7451  cbvmpov  7453  tfis  7797  tfindes  7805  peano5  7835  findes  7842  dfoprab4f  8000  fmpox  8011  xpord2indlem  8089  poseq  8100  soseq  8101  smogt  8299  resixpfo  8874  ixpsnf1o  8876  dom2lem  8929  mapsnend  8973  pw2f1olem  9009  pssnn  9093  ssfi  9097  findcard3  9183  ordiso2  9420  elirrvOLD  9503  cantnflem1d  9597  cantnf  9602  setind  9656  frinsg  9663  tz9.12lem3  9701  infxpen  9924  dfac5lem4  10036  dfac12lem2  10055  kmlem14  10074  cfsmolem  10180  sornom  10187  isf32lem9  10271  axdc2  10359  fpwwe2lem7  10548  fpwwe2  10554  wunex2  10649  dedekindle  11297  wloglei  11669  uzind4s  12821  seqof2  13983  reuccatpfxs1  14670  shftfn  14996  rexuz3  15272  zsum  15641  fsum  15643  sumss  15647  sumss2  15649  fsumcvg2  15650  fsumser  15653  fsumclf  15661  fsumsplitf  15665  isumless  15768  prodfdiv  15819  cbvprod  15836  cbvprodv  15837  zprod  15860  fprod  15864  fprodntriv  15865  prodss  15870  fprod2dlem  15903  fproddivf  15910  fprodsplitf  15911  rpnnen2lem10  16148  cpnnen  16154  sumeven  16314  sumodd  16315  sadcp1  16382  smupp1  16407  pcmptdvds  16822  prmreclem2  16845  prmreclem5  16848  prmreclem6  16849  prmrec  16850  prmdvdsprmo  16970  iscatd2  17604  initoeu2  17940  yoniso  18208  sgrpidmnd  18664  mndind  18753  eqg0subg  19125  symggen  19399  dprd2d2  19975  srhmsubc  20613  isdrngrd  20699  isdrngrdOLD  20701  lbspss  21034  frlmphl  21736  frlmup1  21753  opsrtoslem1  22010  mdetralt  22552  mdetralt2  22553  mdetunilem2  22557  maducoeval2  22584  chfacfscmulgsum  22804  chfacfpmmulgsum  22808  isclo2  23032  neiptopnei  23076  ptcldmpt  23558  elmptrab  23771  hausflimi  23924  hausflim  23925  alexsubALTlem3  23993  alexsubALTlem4  23994  ptcmplem2  23997  cnextcn  24011  cnextfres1  24012  tgphaus  24061  ustuqtop  24190  utopsnneip  24192  ucncn  24228  nrmmetd  24518  xrhmeo  24900  iscau2  25233  caucfil  25239  cmetcaulem  25244  bcth  25285  vitalilem3  25567  vitali  25570  i1f1lem  25646  itg11  25648  i1fres  25662  mbfi1fseq  25678  mbfi1flim  25680  itg2uba  25700  itg2splitlem  25705  isibl2  25723  cbvitg  25733  cbvitgv  25734  itgss3  25772  dvmptfsum  25935  rolle  25950  elply2  26157  plyexmo  26277  lgamgulmlem2  26996  prmorcht  27144  pclogsum  27182  dchr1  27224  lgsdir  27299  lgsdilem2  27300  lgsdi  27301  lgsne0  27302  lgsquadlem3  27349  lgsquad  27350  2sqlem8  27393  nosupcbv  27670  nosupno  27671  nosupdm  27672  nosupbnd1lem1  27676  noinfcbv  27685  noinfno  27686  noinfdm  27687  nocvxminlem  27750  legval  28656  legov  28657  tglineintmo  28714  tglowdim2ln  28723  ishpg  28831  lnopp2hpgb  28835  hpgerlem  28837  colopp  28841  axcontlem1  29037  numedglnl  29217  uvtxnbgrvtx  29466  cusgrres  29522  wspniunwspnon  29996  rusgrnumwwlkb0  30047  frgr3vlem2  30349  3vfriswmgrlem  30352  fusgr2wsp2nb  30409  numclwlk2lem2f1o  30454  lpni  30555  pjhthmo  31377  chscllem2  31713  cbvdisjf  32646  2ndresdju  32727  fmptcof2  32735  aciunf1lem  32740  funcnv4mpt  32747  suppovss  32760  fpwrelmapffslem  32811  fsumiunle  32910  gsumwrd2dccatlem  33159  elrspunsn  33510  1arithufdlem3  33627  fedgmullem1  33786  fldextrspunlsp  33831  extdgfialglem2  33850  zarclssn  34030  esumcvg  34243  fiunelros  34331  measiun  34375  bnj1146  34947  bnj1185  34949  bnj1385  34988  bnj1014  35117  bnj1112  35139  bnj1123  35142  bnj1228  35167  bnj1326  35182  bnj1321  35183  bnj1384  35188  bnj1417  35197  bnj1497  35216  trssfir1om  35267  r1omhfb  35268  fineqvnttrclse  35280  axregscl  35284  setindregs  35286  trssfir1omregs  35292  r1omhfbregs  35293  onvf1odlem2  35298  onvf1odlem3  35299  gonarlem  35588  goalrlem  35590  goalr  35591  mrsubrn  35707  dfon2lem6  35980  dfbigcup2  36091  lineintmo  36351  cbvralvw2  36420  cbvrexvw2  36421  cbvrmovw2  36422  cbvreuvw2  36423  cbvmptvw2  36428  cbvprodvw2  36441  cbvrmodavw  36446  cbvreudavw  36447  cbvrabdavw  36455  cbvmptdavw  36461  cbvriotadavw  36464  cbvixpdavw  36472  cbvproddavw  36474  cbvitgdavw  36475  cbvrabdavw2  36479  cbvmptdavw2  36482  cbvriotadavw2  36484  weiunlem  36657  eleq2w2ALT  37248  bj-idres  37365  mptsnunlem  37543  ptrest  37820  poimirlem25  37846  mblfinlem2  37859  mblfinlem3  37860  mblfinlem4  37861  ismblfin  37862  mbfposadd  37868  itg2addnclem  37872  ftc1anclem5  37898  ftc1anclem6  37899  ftc1anclem7  37900  ftc1anc  37902  areacirclem5  37913  fdc1  37947  inxprnres  38491  fsumshftd  39212  pmapglb  40030  polval2N  40166  osumcllem4N  40219  pexmidlem1N  40230  dih1dimatlem  41589  mapdh9a  42049  mapdh9aOLDN  42050  sticksstones2  42401  selvvvval  42828  fsuppind  42833  fphpd  43058  fphpdo  43059  pellex  43077  setindtrs  43267  dford3lem2  43269  fnwe2lem2  43293  mendlmod  43431  cantnfub  43563  tfsconcat0i  43587  rababg  43815  fsovrfovd  44250  fsovcnvlem  44254  scottabf  44481  trfr  45203  elunif  45261  iunincfi  45338  cbvmpo2  45341  cbvmpo1  45342  disjf1  45427  wessf1ornlem  45429  disjinfi  45436  supxrleubrnmptf  45695  monoordxr  45726  monoord2xr  45728  fsummulc1f  45817  fsumnncl  45818  fsumf1of  45820  fsumiunss  45821  fsumreclf  45822  fsumlessf  45823  fsumsermpt  45825  fmulcl  45827  fmul01lt1lem2  45831  fprodexp  45840  fprodabs2  45841  climmulf  45850  climexp  45851  climrecf  45855  climinff  45857  climaddf  45861  mullimc  45862  limcperiod  45874  sumnnodd  45876  neglimc  45891  addlimc  45892  climsubmpt  45904  climreclf  45908  climeldmeqmpt  45912  climfveqmpt  45915  fnlimfvre  45918  climfveqf  45924  climfveqmpt3  45926  climeldmeqf  45927  climeqf  45932  climeldmeqmpt3  45933  climinf2  45951  limsupequz  45967  limsupequzmptf  45975  lmbr3  45991  cnrefiisp  46074  cncfshift  46118  fprodcncf  46144  dvmptmulf  46181  dvmptfprod  46189  dvnprodlem1  46190  dvnprodlem3  46192  stoweidlem16  46260  stoweidlem34  46278  stoweidlem62  46306  dirkercncflem2  46348  fourierdlem12  46363  fourierdlem15  46366  fourierdlem34  46385  fourierdlem50  46400  fourierdlem73  46423  fourierdlem94  46444  fourierdlem112  46462  fourierdlem113  46463  intsaluni  46573  sge0lempt  46654  sge0iunmptlemfi  46657  sge0iunmptlemre  46659  sge0iunmpt  46662  sge0ltfirpmpt2  46670  sge0isummpt2  46676  sge0xaddlem2  46678  sge0xadd  46679  meadjiun  46710  voliunsge0lem  46716  meaiuninclem  46724  meaiunincf  46727  meaiuninc3v  46728  meaiuninc3  46729  meaiininclem  46730  meaiininc  46731  isomennd  46775  ovn0lem  46809  sge0hsphoire  46833  hoidmvlelem1  46839  hoidmvlelem2  46840  hoidmvlelem3  46841  hoidmvlelem5  46843  hspmbllem2  46871  hoimbl2  46909  vonhoire  46916  vonioo  46926  vonicc  46929  vonn0ioo2  46934  vonn0icc2  46936  pimincfltioc  46960  salpreimagtlt  46974  smflimlem4  47018  ormkglobd  47119  sinnpoly  47137  rexrsb  47346  ichexmpl2  47716  ichnreuop  47718  sbgoldbm  48030  bgoldbnnsum3prm  48050  tgoldbach  48063  srhmsubcALTV  48571  cbvmpox2  48582  mo0sn  49061  f1omoOLD  49139  isthincd2lem1  49670  thincmo  49673  euendfunc  49771