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

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

This syntactical construction introduces a binary non-logical predicate symbol  e. (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  e. 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 1758 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 1757. This lets us avoid overloading the  e. connective, thus preventing ambiguity that would complicate certain Metamath parsers. However, logically wel 1758 is considered to be a primitive syntax, even though here it is artificially "derived" from wcel 1757. 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  x  e.  y

Proof of Theorem wel
StepHypRef Expression
1 wcel 1757 1  wff  x  e.  y
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1757
This theorem is referenced by:  elequ1  1760  elequ2  1762  ax12wdemo  1770  cleljust  2065  cleljustALT  2066  dveel1  2067  dveel2  2068  axc14  2069  elsb3  2145  elsb4  2146  ax5el  2244  dveel2ALT  2246  ax12el  2249  axext2  2430  axext3  2431  axext4  2432  bm1.1  2433  bm1.1OLD  2434  ru  3269  nfuni  4181  nfunid  4182  unieq  4183  csbuni  4203  inteq  4215  nfint  4222  uniiun  4307  intiin  4308  trint  4484  trintss  4485  axrep1  4488  axrep2  4489  axrep3  4490  axrep4  4491  axrep5  4492  zfrepclf  4493  axsep  4496  axsep2  4498  bm1.3ii  4500  zfnuleu  4502  0ex  4506  nalset  4513  axpweq  4553  zfpow  4555  axpow2  4556  axpow3  4557  el  4558  dtru  4567  nfnid  4605  dvdemo1  4611  dvdemo2  4612  dfepfr  4789  wetrep  4797  wefrc  4798  ordelord  4825  rele  5052  funimaexg  5579  zfun  6459  axun2  6460  uniuni  6471  onint  6492  ordom  6571  dfsmo2  6894  smores2  6901  smo11  6911  smogt  6914  tz7.48lem  6982  tz7.48-2  6983  omeulem1  7107  pw2eng  7503  infensuc  7575  1sdom  7602  unxpdomlem1  7604  unxpdomlem2  7605  unxpdomlem3  7606  pssnn  7618  findcard2  7639  findcard2d  7641  ac6sfi  7643  frfi  7644  fissuni  7703  axreg2  7895  zfregcl  7896  dford2  7913  inf0  7914  inf1  7915  inf2  7916  zfinf  7932  axinf2  7933  zfinf2  7935  dfom4  7942  dfom5  7943  unbnn3  7951  noinfep  7952  cantnf  7988  cantnfOLD  8010  epfrs  8038  r111  8069  dif1card  8264  alephle  8345  aceq1  8374  aceq0  8375  aceq2  8376  dfac3  8378  dfac5lem2  8381  dfac5lem4  8383  dfac5  8385  dfac2a  8386  dfac2  8387  dfac7  8388  dfac0  8389  dfac1  8390  kmlem3  8408  kmlem4  8409  kmlem5  8410  kmlem8  8413  kmlem14  8419  kmlem15  8420  dfackm  8422  ackbij1lem10  8485  coflim  8517  cflim2  8519  cfsmolem  8526  fin23lem26  8581  ituniiun  8678  domtriomlem  8698  axdc3lem2  8707  zfac  8716  ac2  8717  ac3  8718  axac3  8720  axac2  8722  axac  8723  nd1  8838  nd2  8839  nd3  8840  nd4  8841  axextnd  8842  axrepndlem1  8843  axrepndlem2  8844  axrepnd  8845  axunndlem1  8846  axunnd  8847  axpowndlem1  8848  axpowndlem2  8849  axpowndlem2OLD  8850  axpowndlem3  8851  axpowndlem4  8853  axpownd  8854  axregndlem1  8855  axregndlem2  8856  axregnd  8857  axregndOLD  8858  axinfndlem1  8859  axinfnd  8860  axacndlem1  8861  axacndlem2  8862  axacndlem3  8863  axacndlem4  8864  axacndlem5  8865  axacnd  8866  fpwwe2lem12  8895  axgroth5  9078  axgroth2  9079  grothpw  9080  axgroth6  9082  grothomex  9083  axgroth3  9085  axgroth4  9086  grothprimlem  9087  grothprim  9088  nqereu  9185  npex  9242  elnpi  9244  hashbclem  12293  brfi1uzind  12307  fsum2dlem  13325  rpnnen  13597  ismre  14616  fnmre  14617  mremre  14630  isacs  14677  isacs1i  14683  mreacs  14684  acsfn1  14687  acsfn2  14689  isacs3lem  15424  pmtrprfval  16081  pmtrsn  16113  gsum2dlem2  16553  gsum2dOLD  16555  lbsextlem4  17334  drngnidl  17403  mplcoe1  17637  mplcoe5  17641  mplcoe2OLD  17643  zringlpir  18001  zlpir  18006  mdetunilem9  18528  mdetuni0  18529  maducoeval2  18548  madugsum  18551  isbasis3g  18656  tgcl  18676  tgss2  18694  toponmre  18799  neiptopnei  18838  ist0  19026  ishaus  19028  t0top  19035  haustop  19037  isreg  19038  ist0-2  19050  ist0-3  19051  t1t0  19054  ist1-3  19055  ishaus2  19057  haust1  19058  cmpsublem  19104  cmpsub  19105  tgcmp  19106  hauscmp  19112  bwth  19115  is1stc2  19148  2ndcctbss  19161  2ndcdisj  19162  2ndcdisj2  19163  2ndcomap  19164  2ndcsep  19165  dis2ndc  19166  restnlly  19188  restlly  19189  llyidm  19194  nllyidm  19195  lly1stc  19202  ptpjopn  19287  tx1stc  19325  txkgen  19327  xkohaus  19328  xkococnlem  19334  xkoinjcn  19362  ist0-4  19404  kqt0lem  19411  regr1lem2  19415  kqt0  19421  r0sep  19423  nrmr0reg  19424  regr1  19425  kqreg  19426  kqnrm  19427  kqhmph  19494  filuni  19560  uffinfix  19602  fmfnfmlem4  19632  hauspwpwf1  19662  alexsublem  19718  alexsubALTlem3  19723  alexsubALTlem4  19724  alexsubALT  19725  blbas  20107  met1stc  20198  metrest  20201  xrsmopn  20491  cnheibor  20629  jensen  22484  sqff1o  22622  usgrafis  23449  cusgrasize  23507  dfconngra1  23678  isplig  23785  tncp  23786  spanuni  25068  sumdmdii  25940  indf1o  26600  gsumesum  26630  dya2iocuni  26818  erdsze  27210  conpcon  27244  rellyscon  27260  cvmsss2  27283  cvmlift2lem12  27323  axextprim  27472  axrepprim  27473  axunprim  27474  axpowprim  27475  axregprim  27476  axinfprim  27477  axacprim  27478  untelirr  27479  untuni  27480  untsucf  27481  unt0  27482  untint  27483  untangtr  27485  fprod2dlem  27611  fprod2d  27612  dftr6  27680  dffr5  27683  elpotr  27714  dfon2lem3  27718  dfon2lem4  27719  dfon2lem5  27720  dfon2lem6  27721  dfon2lem7  27722  dfon2lem8  27723  dfon2lem9  27724  dfon2  27725  domep  27726  axextdfeq  27731  ax8dfeq  27732  axextdist  27733  axext4dist  27734  exnel  27736  distel  27737  axextndbi  27738  poseq  27834  wfrlem12  27855  frrlem11  27900  nobndlem6  27958  nofulllem5  27967  dfiota3  28074  brcup  28090  brcap  28091  tfrqfree  28102  dfint3  28103  imagesset  28104  hftr  28340  onsuct0  28407  finixpnum  28538  fin2solem  28539  fin2so  28540  heicant  28550  mblfinlem1  28552  mbfresfi  28562  cnambfre  28564  ftc1anc  28599  ftc2nc  28600  fness  28678  fneref  28680  fnessref  28689  finptfin  28693  locfincmp  28700  comppfsc  28703  neibastop2lem  28705  cover2g  28732  sstotbnd2  28797  unichnidl  28955  prtlem5  29125  prtlem12  29136  prtlem13  29137  prtlem15  29144  prtlem17  29145  prtlem18  29146  prter1  29148  prter3  29151  ismrcd1  29158  dford3lem2  29500  dford4  29502  pw2f1ocnv  29510  pw2f1o2  29511  wepwsolem  29518  fnwe2lem2  29528  aomclem8  29538  kelac1  29540  pwslnm  29571  idomsubgmo  29687  0egra0rgra  30673  dflinc2  31037  lcosslsp  31065  sbcoreleleq  31523  tratrb  31524  ordelordALT  31526  trsbc  31529  truniALT  31530  onfrALTlem5  31532  onfrALTlem4  31533  onfrALTlem3  31534  onfrALTlem2  31536  onfrALTlem1  31538  onfrALT  31539  sspwtrALT  31838  suctrALT2  31855  tratrbVD  31879  truniALTVD  31896  trintALT  31899  onfrALTlem4VD  31904  bnj219  32006  bnj1098  32059  bnj594  32187  bnj580  32188  bnj601  32195  bnj849  32200  bnj996  32230  bnj1006  32234  bnj1029  32241  bnj1033  32242  bnj1090  32252  bnj1110  32255  bnj1124  32261  bnj1128  32263  bj-elequ2g  32455  bj-ax89  32456  bj-elequ12  32457  bj-cleljust  32561  bj-axext3  32571  bj-axext4  32572  bj-clabel  32586  bj-axrep1  32591  bj-axrep2  32592  bj-axrep3  32593  bj-axrep4  32594  bj-axrep5  32595  bj-axsep  32596  bj-nalset  32597  bj-zfpow  32598  bj-el  32599  bj-dtru  32600  bj-dvdemo1  32605  bj-dvdemo2  32606  bj-ax9  32681  bj-dfcleq  32683  bj-axsep2  32710  bj-ru0  32717  bj-ru1  32718  bj-ru  32719  pclfinclN  33876  dvh1dim  35369
  Copyright terms: Public domain W3C validator