MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  wel Structured version   Visualization version   GIF version

Theorem wel 2031
Description: Extend wff definition to include atomic formulas with the epsilon (membership) predicate. This is read "𝑥 is an element of 𝑦," "𝑥 is a member of 𝑦," "𝑥 belongs to 𝑦," or "𝑦 contains 𝑥." Note: The phrase "𝑦 includes 𝑥 " means "𝑥 is a subset of 𝑦;" to use it also for 𝑥𝑦, as some authors occasionally do, is poor form and causes confusion, according to George Boolos (1992 lecture at MIT).

This syntactic construction introduces a binary non-logical predicate symbol (epsilon) into our predicate calculus. We will eventually use it for the membership predicate of set theory, but that is irrelevant at this point: the predicate calculus axioms for apply to any arbitrary binary predicate symbol. "Non-logical" means that the predicate is presumed to have additional properties beyond the realm of predicate calculus, although these additional properties are not specified by predicate calculus itself but rather by the axioms of a theory (in our case set theory) added to predicate calculus. "Binary" means that the predicate has two arguments.

(Instead of introducing wel 2031 as an axiomatic statement, as was done in an older version of this database, we introduce it by "proving" a special case of set theory's more general wcel 2030. This lets us avoid overloading the connective, thus preventing ambiguity that would complicate certain Metamath parsers. However, logically wel 2031 is considered to be a primitive syntax, even though here it is artificially "derived" from wcel 2030. Note: To see the proof steps of this syntax proof, type "show proof wel /all" in the Metamath program.) (Contributed by NM, 24-Jan-2006.)

Assertion
Ref Expression
wel wff 𝑥𝑦

Proof of Theorem wel
StepHypRef Expression
1 wcel 2030 1 wff 𝑥𝑦
Colors of variables: wff setvar class
Syntax hints:  wcel 2030
This theorem is referenced by:  ax8  2036  elequ1  2037  cleljust  2038  ax9  2043  elequ2  2044  ax12wdemo  2052  cleljustALT  2221  cleljustALT2  2222  dveel1  2398  dveel2  2399  axc14  2400  elsb3  2462  elsb4  2463  axext2  2632  axext3  2633  axext3ALT  2634  axext4  2635  bm1.1  2636  sbabel  2822  ru  3467  nfuni  4474  nfunid  4475  unieq  4476  csbuni  4498  inteq  4510  elintg  4515  nfint  4518  int0  4522  intss  4530  uniiun  4605  intiin  4606  trint  4801  trintssOLD  4803  axrep1  4805  axrep2  4806  axrep3  4807  axrep4  4808  axrep5  4809  zfrepclf  4810  axsep  4813  axsep2  4815  bm1.3ii  4817  zfnuleu  4819  axnul  4821  0ex  4823  nalset  4828  axpweq  4872  zfpow  4874  axpow2  4875  axpow3  4876  el  4877  dtru  4887  nfnid  4927  dvdemo1  4932  dvdemo2  4933  dfepfr  5128  wetrep  5136  wefrc  5137  rele  5283  ordelord  5783  onfr  5801  funimaexg  6013  zfun  6992  axun2  6993  uniuni  7013  onint  7037  ordom  7116  wfrlem12  7471  dfsmo2  7489  smores2  7496  smo11  7506  smogt  7509  dfrecs3  7514  tz7.48lem  7581  tz7.48-2  7582  omeulem1  7707  pw2eng  8107  infensuc  8179  1sdom  8204  unxpdomlem1  8205  unxpdomlem2  8206  unxpdomlem3  8207  pssnn  8219  findcard2  8241  findcard2d  8243  ac6sfi  8245  frfi  8246  fissuni  8312  axreg2  8539  zfregcl  8540  dford2  8555  inf0  8556  inf1  8557  inf2  8558  zfinf  8574  axinf2  8575  zfinf2  8577  dfom4  8584  dfom5  8585  unbnn3  8594  noinfep  8595  cantnf  8628  epfrs  8645  r111  8676  dif1card  8871  alephle  8949  aceq1  8978  aceq0  8979  aceq2  8980  dfac3  8982  dfac5lem2  8985  dfac5lem4  8987  dfac5  8989  dfac2a  8990  dfac2  8991  dfac7  8992  dfac0  8993  dfac1  8994  kmlem3  9012  kmlem4  9013  kmlem5  9014  kmlem8  9017  kmlem14  9023  kmlem15  9024  dfackm  9026  ackbij1lem10  9089  coflim  9121  cflim2  9123  cfsmolem  9130  fin23lem26  9185  ituniiun  9282  domtriomlem  9302  axdc3lem2  9311  zfac  9320  ac2  9321  ac3  9322  axac3  9324  axac2  9326  axac  9327  nd1  9447  nd2  9448  nd3  9449  nd4  9450  axextnd  9451  axrepndlem1  9452  axrepndlem2  9453  axrepnd  9454  axunndlem1  9455  axunnd  9456  axpowndlem1  9457  axpowndlem2  9458  axpowndlem3  9459  axpowndlem4  9460  axpownd  9461  axregndlem1  9462  axregndlem2  9463  axregnd  9464  axinfndlem1  9465  axinfnd  9466  axacndlem1  9467  axacndlem2  9468  axacndlem3  9469  axacndlem4  9470  axacndlem5  9471  axacnd  9472  fpwwe2lem12  9501  inar1  9635  axgroth5  9684  axgroth2  9685  grothpw  9686  axgroth6  9688  grothomex  9689  axgroth3  9691  axgroth4  9692  grothprimlem  9693  grothprim  9694  nqereu  9789  npex  9846  elnpi  9848  hashbclem  13274  fsum2dlem  14545  fprod2dlem  14754  fprod2d  14755  rpnnen2  14999  lcmfunsnlem2lem2  15399  ismre  16297  fnmre  16298  mremre  16311  isacs  16359  isacs1i  16365  mreacs  16366  acsfn1  16369  acsfn2  16371  isacs3lem  17213  pmtrprfval  17953  pmtrsn  17985  gsum2dlem2  18416  lbsextlem4  19209  drngnidl  19277  mplcoe1  19513  mplcoe5  19516  mdetunilem9  20474  mdetuni0  20475  maducoeval2  20494  madugsum  20497  isbasis3g  20801  tgcl  20821  tgss2  20839  toponmre  20945  neiptopnei  20984  ist0  21172  ishaus  21174  t0top  21181  haustop  21183  isreg  21184  ist0-2  21196  ist0-3  21197  t1t0  21200  ist1-3  21201  ishaus2  21203  haust1  21204  cmpsublem  21250  cmpsub  21251  tgcmp  21252  hauscmp  21258  bwth  21261  is1stc2  21293  2ndcctbss  21306  2ndcdisj  21307  2ndcdisj2  21308  2ndcomap  21309  2ndcsep  21310  dis2ndc  21311  restnlly  21333  restlly  21334  llyidm  21339  nllyidm  21340  lly1stc  21347  finptfin  21369  locfincmp  21377  ptpjopn  21463  tx1stc  21501  txkgen  21503  xkohaus  21504  xkococnlem  21510  xkoinjcn  21538  ist0-4  21580  kqt0lem  21587  regr1lem2  21591  kqt0  21597  r0sep  21599  nrmr0reg  21600  regr1  21601  kqreg  21602  kqnrm  21603  kqhmph  21670  isfil  21698  filuni  21736  isufil  21754  uffinfix  21778  fmfnfmlem4  21808  hauspwpwf1  21838  alexsublem  21895  alexsubALTlem3  21900  alexsubALTlem4  21901  alexsubALT  21902  ustval  22053  isust  22054  blbas  22282  met1stc  22373  metrest  22376  xrsmopn  22662  cnheibor  22801  jensen  24760  sqff1o  24953  uhgrnbgr0nb  26295  rusgrpropedg  26536  isplig  27458  ispligb  27459  tncp  27460  l2p  27461  eulplig  27467  spanuni  28531  sumdmdii  29402  gsumvsca2  29911  indf1o  30214  gsumesum  30249  dya2iocuni  30473  bnj219  30927  bnj1098  30980  bnj594  31108  bnj580  31109  bnj601  31116  bnj849  31121  bnj996  31151  bnj1006  31155  bnj1029  31162  bnj1033  31163  bnj1090  31173  bnj1110  31176  bnj1124  31182  bnj1128  31184  erdsze  31310  connpconn  31343  rellysconn  31359  cvmsss2  31382  cvmlift2lem12  31422  axextprim  31704  axrepprim  31705  axunprim  31706  axpowprim  31707  axregprim  31708  axinfprim  31709  axacprim  31710  untelirr  31711  untuni  31712  untsucf  31713  unt0  31714  untint  31715  untangtr  31717  dftr6  31766  dffr5  31769  elpotr  31810  dfon2lem3  31814  dfon2lem4  31815  dfon2lem5  31816  dfon2lem6  31817  dfon2lem7  31818  dfon2lem8  31819  dfon2lem9  31820  dfon2  31821  domep  31822  axextdfeq  31827  ax8dfeq  31828  axextdist  31829  axext4dist  31830  exnel  31832  distel  31833  axextndbi  31834  poseq  31878  frrlem4  31908  frrlem11  31917  nosupno  31974  dfiota3  32155  brcup  32171  brcap  32172  dfint3  32184  imagesset  32185  hftr  32414  fness  32469  fneref  32470  neibastop2lem  32480  onsuct0  32565  bj-elequ2g  32791  bj-ax89  32792  bj-elequ12  32793  bj-cleljusti  32794  bj-axext3  32894  bj-axext4  32895  bj-clabel  32908  bj-axrep1  32913  bj-axrep2  32914  bj-axrep3  32915  bj-axrep4  32916  bj-axrep5  32917  bj-axsep  32918  bj-nalset  32919  bj-zfpow  32920  bj-el  32921  bj-dtru  32922  bj-dvdemo1  32927  bj-dvdemo2  32928  bj-nfeel2  32962  bj-axc14nf  32963  bj-axc14  32964  bj-ax8  33012  bj-dfclel  33014  bj-ax9  33015  bj-ax9-2  33016  bj-cleqhyp  33017  bj-dfcleq  33019  bj-axsep2  33046  bj-ru0  33057  bj-ru1  33058  bj-ru  33059  bj-nul  33143  bj-nuliota  33144  bj-nuliotaALT  33145  finixpnum  33524  fin2solem  33525  fin2so  33526  matunitlindflem1  33535  poimirlem30  33569  poimirlem32  33571  poimir  33572  mblfinlem1  33576  mbfresfi  33586  cnambfre  33588  ftc1anc  33623  ftc2nc  33624  cover2g  33639  sstotbnd2  33703  unichnidl  33960  prtlem5  34464  prtlem12  34471  prtlem13  34472  prtlem15  34479  prtlem17  34480  prtlem18  34481  prter1  34483  prter3  34486  ax5el  34541  dveel2ALT  34543  ax12el  34546  pclfinclN  35554  dvh1dim  37048  ismrcd1  37578  dford3lem2  37911  dford4  37913  pw2f1ocnv  37921  pw2f1o2  37922  wepwsolem  37929  fnwe2lem2  37938  aomclem8  37948  kelac1  37950  pwslnm  37981  idomsubgmo  38093  inintabss  38201  inintabd  38202  cnvcnvintabd  38223  intabssd  38233  elintima  38262  dffrege76  38550  frege77  38551  frege89  38563  frege90  38564  frege91  38565  frege93  38567  frege94  38568  frege95  38569  clsk1indlem3  38658  ntrneiel2  38701  ntrneik2  38707  ntrneix2  38708  ntrneik4  38716  gneispa  38745  gneispace2  38747  gneispace3  38748  gneispace  38749  gneispacef  38750  gneispacef2  38751  gneispacern2  38754  gneispace0nelrn  38755  gneispaceel  38758  gneispaceel2  38759  gneispacess  38760  sbcoreleleq  39062  tratrb  39063  ordelordALT  39064  trsbc  39067  truniALT  39068  onfrALTlem5  39074  onfrALTlem4  39075  onfrALTlem3  39076  onfrALTlem2  39078  onfrALTlem1  39080  onfrALT  39081  sspwtrALT  39366  suctrALT2  39386  tratrbVD  39411  truniALTVD  39428  trintALT  39431  onfrALTlem4VD  39436  dfnelbr2  41614  nelbr  41615  nelbrim  41616  sprsymrelf1lem  42066  sprsymrelf  42070  dflinc2  42524  lcosslsp  42552  nfintd  42745
  Copyright terms: Public domain W3C validator