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

Theorem wel 1718
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 1718 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 1717. This lets us avoid overloading the  e. connective, thus preventing ambiguity that would complicate certain Metamath parsers. However, logically wel 1718 is considered to be a primitive syntax, even though here it is artificially "derived" from wcel 1717. 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 1717 1  wff  x  e.  y
Colors of variables: wff set class
Syntax hints:    e. wcel 1717
This theorem is referenced by:  elequ1  1720  elequ2  1722  ax11wdemo  1730  cleljust  2048  cleljustALT  2049  dveel1  2052  dveel2  2053  ax15  2054  elsb3  2136  elsb4  2137  ax17el  2223  dveel2ALT  2225  ax11el  2228  axext2  2369  axext3  2370  axext4  2371  bm1.1  2372  ru  3103  nfuni  3963  nfunid  3964  unieq  3966  inteq  3995  nfint  4002  uniiun  4085  intiin  4086  trint  4258  trintss  4259  axrep1  4262  axrep2  4263  axrep3  4264  axrep4  4265  axrep5  4266  zfrepclf  4267  axsep  4270  axsep2  4272  bm1.3ii  4274  zfnuleu  4276  0ex  4280  nalset  4281  axpweq  4317  zfpow  4319  axpow2  4320  axpow3  4321  el  4322  dtru  4331  nfnid  4334  dvdemo1  4340  dvdemo2  4341  dfepfr  4508  wetrep  4516  wefrc  4517  ordelord  4544  zfun  4642  axun2  4643  uniuni  4656  onint  4715  ordom  4794  rele  4943  funimaexg  5470  dfsmo2  6545  smores2  6552  smo11  6562  smogt  6565  tz7.48lem  6634  tz7.48-2  6635  omeulem1  6761  pw2eng  7150  infensuc  7221  1sdom  7247  unxpdomlem1  7249  unxpdomlem2  7250  unxpdomlem3  7251  pssnn  7263  findcard2  7284  ac6sfi  7287  frfi  7288  fissuni  7346  axreg2  7494  zfregcl  7495  ruv  7501  dford2  7508  inf0  7509  inf1  7510  inf2  7511  zfinf  7527  axinf2  7528  zfinf2  7530  dfom4  7537  dfom5  7538  unbnn3  7546  noinfep  7547  cantnf  7582  epfrs  7600  r111  7634  dif1card  7825  alephle  7902  aceq1  7931  aceq0  7932  aceq2  7933  dfac3  7935  dfac5lem2  7938  dfac5lem4  7940  dfac5  7942  dfac2a  7943  dfac2  7944  dfac7  7945  dfac0  7946  dfac1  7947  kmlem3  7965  kmlem4  7966  kmlem5  7967  kmlem8  7970  kmlem14  7976  kmlem15  7977  dfackm  7979  ackbij1lem10  8042  coflim  8074  cflim2  8076  cfsmolem  8083  fin23lem26  8138  ituniiun  8235  domtriomlem  8255  axdc3lem2  8264  zfac  8273  ac2  8274  ac3  8275  axac3  8277  axac2  8279  axac  8280  nd1  8395  nd2  8396  nd3  8397  nd4  8398  axextnd  8399  axrepndlem1  8400  axrepndlem2  8401  axrepnd  8402  axunndlem1  8403  axunnd  8404  axpowndlem1  8405  axpowndlem2  8406  axpowndlem4  8408  axpownd  8409  axregndlem1  8410  axregndlem2  8411  axregnd  8412  axinfndlem1  8413  axinfnd  8414  axacndlem1  8415  axacndlem2  8416  axacndlem3  8417  axacndlem4  8418  axacndlem5  8419  axacnd  8420  fpwwe2lem12  8449  axgroth5  8632  axgroth2  8633  grothpw  8634  axgroth6  8636  grothomex  8637  axgroth3  8639  axgroth4  8640  grothprimlem  8641  grothprim  8642  nqereu  8739  npex  8796  elnpi  8798  hashbclem  11628  brfi1uzind  11642  fsum2dlem  12481  rpnnen  12753  ismre  13742  fnmre  13743  mremre  13756  isacs  13803  isacs1i  13809  mreacs  13810  acsfn1  13813  acsfn2  13815  isacs3lem  14519  gsum2d  15473  lbsextlem4  16160  drngnidl  16227  mplcoe1  16455  mplcoe2  16457  zlpir  16694  isbasis3g  16937  tgcl  16957  tgss2  16975  toponmre  17080  neiptopnei  17119  ist0  17306  ishaus  17308  t0top  17315  haustop  17317  isreg  17318  ist0-2  17330  ist0-3  17331  t1t0  17334  ist1-3  17335  ishaus2  17337  haust1  17338  cmpsublem  17384  cmpsub  17385  tgcmp  17386  hauscmp  17392  is1stc2  17426  2ndcctbss  17439  2ndcdisj  17440  2ndcdisj2  17441  2ndcomap  17442  2ndcsep  17443  dis2ndc  17444  restnlly  17466  restlly  17467  llyidm  17472  nllyidm  17473  lly1stc  17480  ptpjopn  17565  tx1stc  17603  txkgen  17605  xkohaus  17606  xkococnlem  17612  xkoinjcn  17640  ist0-4  17682  kqt0lem  17689  regr1lem2  17693  kqt0  17699  r0sep  17701  nrmr0reg  17702  regr1  17703  kqreg  17704  kqnrm  17705  kqhmph  17772  filuni  17838  uffinfix  17880  fmfnfmlem4  17910  hauspwpwf1  17940  alexsublem  17996  alexsubALTlem3  18001  alexsubALTlem4  18002  alexsubALT  18003  blbas  18350  met1stc  18441  metrest  18444  xrsmopn  18714  cnheibor  18851  jensen  20694  sqff1o  20832  usgrafis  21295  cusgrasize  21353  dfconngra1  21506  isplig  21613  tncp  21614  spanuni  22894  sumdmdii  23766  indf1o  24217  gsumesum  24247  dya2iocuni  24427  erdsze  24667  conpcon  24701  rellyscon  24717  cvmsss2  24740  cvmlift2lem12  24780  axextprim  24929  axrepprim  24930  axunprim  24931  axpowprim  24932  axregprim  24933  axinfprim  24934  axacprim  24935  untelirr  24936  untuni  24937  untsucf  24938  unt0  24939  untint  24940  untangtr  24942  dftr6  25131  dffr5  25134  elpotr  25161  dfon2lem3  25165  dfon2lem4  25166  dfon2lem5  25167  dfon2lem6  25168  dfon2lem7  25169  dfon2lem8  25170  dfon2lem9  25171  dfon2  25172  domep  25173  axextdfeq  25178  ax13dfeq  25179  axextdist  25180  axext4dist  25181  exnel  25183  distel  25184  axextndbi  25185  poseq  25277  wfrlem12  25291  tfrALTlem  25300  frrlem11  25317  nobndlem6  25375  nofulllem5  25384  dfiota3  25486  tfrqfree  25514  hftr  25837  onsuct0  25905  fness  26053  fneref  26055  fnessref  26064  finptfin  26068  locfincmp  26075  comppfsc  26078  neibastop2lem  26080  cover2g  26107  sstotbnd2  26174  unichnidl  26332  prtlem5  26396  prtlem12  26407  prtlem13  26408  prtlem15  26415  prtlem17  26416  prtlem18  26417  prter1  26419  prter3  26422  ismrcd1  26443  dford3lem2  26789  dford4  26791  pw2f1ocnv  26799  pw2f1o2  26800  wepwsolem  26807  fnwe2lem2  26817  aomclem8  26828  kelac1  26830  pwslnm  26865  idomsubgmo  27183  sbcoreleleq  27962  tratrb  27963  ordelordALT  27965  trsbc  27968  truniALT  27969  onfrALTlem5  27971  onfrALTlem4  27972  onfrALTlem3  27973  onfrALTlem2  27975  onfrALTlem1  27977  onfrALT  27978  sspwtrALT  28276  suctrALT2  28290  tratrbVD  28314  truniALTVD  28331  trintALT  28334  onfrALTlem4VD  28339  bnj219  28438  bnj1098  28492  bnj594  28621  bnj580  28622  bnj601  28629  bnj849  28634  bnj996  28664  bnj1006  28668  bnj1029  28675  bnj1033  28676  bnj1090  28686  bnj1110  28689  bnj1124  28695  bnj1128  28697  dveel1NEW7  28803  dveel2NEW7  28804  ax15NEW7  28872  elsb3NEW7  28936  elsb4NEW7  28937  cleljustNEW7  28960  pclfinclN  30064  dvh1dim  31557
  Copyright terms: Public domain W3C validator