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

Theorem wel 1768
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 1768 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 1767. This lets us avoid overloading the  e. connective, thus preventing ambiguity that would complicate certain Metamath parsers. However, logically wel 1768 is considered to be a primitive syntax, even though here it is artificially "derived" from wcel 1767. 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 1767 1  wff  x  e.  y
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1767
This theorem is referenced by:  elequ1  1770  elequ2  1772  ax12wdemo  1780  cleljust  2082  cleljustALT  2083  dveel1  2084  dveel2  2085  axc14  2086  elsb3  2161  elsb4  2162  ax5el  2260  dveel2ALT  2262  ax12el  2265  axext2  2446  axext3  2447  axext3OLD  2448  axext4  2449  bm1.1  2450  bm1.1OLD  2451  sbabel  2660  ru  3330  nfuni  4251  nfunid  4252  unieq  4253  csbuni  4273  inteq  4285  nfint  4292  uniiun  4378  intiin  4379  trint  4555  trintss  4556  axrep1  4559  axrep2  4560  axrep3  4561  axrep4  4562  axrep5  4563  zfrepclf  4564  axsep  4567  axsep2  4569  bm1.3ii  4571  zfnuleu  4573  0ex  4577  nalset  4584  axpweq  4624  zfpow  4626  axpow2  4627  axpow3  4628  el  4629  dtru  4638  nfnid  4676  dvdemo1  4682  dvdemo2  4683  dfepfr  4864  wetrep  4872  wefrc  4873  ordelord  4900  rele  5129  funimaexg  5663  zfun  6575  axun2  6576  uniuni  6587  onint  6608  ordom  6687  dfsmo2  7015  smores2  7022  smo11  7032  smogt  7035  tz7.48lem  7103  tz7.48-2  7104  omeulem1  7228  pw2eng  7620  infensuc  7692  1sdom  7719  unxpdomlem1  7721  unxpdomlem2  7722  unxpdomlem3  7723  pssnn  7735  findcard2  7756  findcard2d  7758  ac6sfi  7760  frfi  7761  fissuni  7821  axreg2  8015  zfregcl  8016  dford2  8033  inf0  8034  inf1  8035  inf2  8036  zfinf  8052  axinf2  8053  zfinf2  8055  dfom4  8062  dfom5  8063  unbnn3  8071  noinfep  8072  cantnf  8108  cantnfOLD  8130  epfrs  8158  r111  8189  dif1card  8384  alephle  8465  aceq1  8494  aceq0  8495  aceq2  8496  dfac3  8498  dfac5lem2  8501  dfac5lem4  8503  dfac5  8505  dfac2a  8506  dfac2  8507  dfac7  8508  dfac0  8509  dfac1  8510  kmlem3  8528  kmlem4  8529  kmlem5  8530  kmlem8  8533  kmlem14  8539  kmlem15  8540  dfackm  8542  ackbij1lem10  8605  coflim  8637  cflim2  8639  cfsmolem  8646  fin23lem26  8701  ituniiun  8798  domtriomlem  8818  axdc3lem2  8827  zfac  8836  ac2  8837  ac3  8838  axac3  8840  axac2  8842  axac  8843  nd1  8958  nd2  8959  nd3  8960  nd4  8961  axextnd  8962  axrepndlem1  8963  axrepndlem2  8964  axrepnd  8965  axunndlem1  8966  axunnd  8967  axpowndlem1  8968  axpowndlem2  8969  axpowndlem2OLD  8970  axpowndlem3  8971  axpowndlem4  8973  axpownd  8974  axregndlem1  8975  axregndlem2  8976  axregnd  8977  axregndOLD  8978  axinfndlem1  8979  axinfnd  8980  axacndlem1  8981  axacndlem2  8982  axacndlem3  8983  axacndlem4  8984  axacndlem5  8985  axacnd  8986  fpwwe2lem12  9015  axgroth5  9198  axgroth2  9199  grothpw  9200  axgroth6  9202  grothomex  9203  axgroth3  9205  axgroth4  9206  grothprimlem  9207  grothprim  9208  nqereu  9303  npex  9360  elnpi  9362  hashbclem  12463  brfi1uzind  12494  fsum2dlem  13544  rpnnen  13817  ismre  14841  fnmre  14842  mremre  14855  isacs  14902  isacs1i  14908  mreacs  14909  acsfn1  14912  acsfn2  14914  isacs3lem  15649  pmtrprfval  16308  pmtrsn  16340  gsum2dlem2  16789  gsum2dOLD  16791  lbsextlem4  17590  drngnidl  17659  mplcoe1  17898  mplcoe5  17902  mplcoe2OLD  17904  zringlpir  18279  zlpir  18284  mdetunilem9  18889  mdetuni0  18890  maducoeval2  18909  madugsum  18912  isbasis3g  19217  tgcl  19237  tgss2  19255  toponmre  19360  neiptopnei  19399  ist0  19587  ishaus  19589  t0top  19596  haustop  19598  isreg  19599  ist0-2  19611  ist0-3  19612  t1t0  19615  ist1-3  19616  ishaus2  19618  haust1  19619  cmpsublem  19665  cmpsub  19666  tgcmp  19667  hauscmp  19673  bwth  19676  is1stc2  19709  2ndcctbss  19722  2ndcdisj  19723  2ndcdisj2  19724  2ndcomap  19725  2ndcsep  19726  dis2ndc  19727  restnlly  19749  restlly  19750  llyidm  19755  nllyidm  19756  lly1stc  19763  ptpjopn  19848  tx1stc  19886  txkgen  19888  xkohaus  19889  xkococnlem  19895  xkoinjcn  19923  ist0-4  19965  kqt0lem  19972  regr1lem2  19976  kqt0  19982  r0sep  19984  nrmr0reg  19985  regr1  19986  kqreg  19987  kqnrm  19988  kqhmph  20055  filuni  20121  uffinfix  20163  fmfnfmlem4  20193  hauspwpwf1  20223  alexsublem  20279  alexsubALTlem3  20284  alexsubALTlem4  20285  alexsubALT  20286  blbas  20668  met1stc  20759  metrest  20762  xrsmopn  21052  cnheibor  21190  jensen  23046  sqff1o  23184  usgrafis  24091  cusgrasize  24154  dfconngra1  24347  0egra0rgra  24612  isplig  24855  tncp  24856  spanuni  26138  sumdmdii  27010  gsumvsca2  27437  indf1o  27677  gsumesum  27707  dya2iocuni  27894  erdsze  28286  conpcon  28320  rellyscon  28336  cvmsss2  28359  cvmlift2lem12  28399  axextprim  28548  axrepprim  28549  axunprim  28550  axpowprim  28551  axregprim  28552  axinfprim  28553  axacprim  28554  untelirr  28555  untuni  28556  untsucf  28557  unt0  28558  untint  28559  untangtr  28561  fprod2dlem  28687  fprod2d  28688  dftr6  28756  dffr5  28759  elpotr  28790  dfon2lem3  28794  dfon2lem4  28795  dfon2lem5  28796  dfon2lem6  28797  dfon2lem7  28798  dfon2lem8  28799  dfon2lem9  28800  dfon2  28801  domep  28802  axextdfeq  28807  ax8dfeq  28808  axextdist  28809  axext4dist  28810  exnel  28812  distel  28813  axextndbi  28814  poseq  28910  wfrlem12  28931  frrlem11  28976  nobndlem6  29034  nofulllem5  29043  dfiota3  29150  brcup  29166  brcap  29167  tfrqfree  29178  dfint3  29179  imagesset  29180  hftr  29416  onsuct0  29483  finixpnum  29615  fin2solem  29616  fin2so  29617  heicant  29626  mblfinlem1  29628  mbfresfi  29638  cnambfre  29640  ftc1anc  29675  ftc2nc  29676  fness  29754  fneref  29756  fnessref  29765  finptfin  29769  locfincmp  29776  comppfsc  29779  neibastop2lem  29781  cover2g  29808  sstotbnd2  29873  unichnidl  30031  prtlem5  30201  prtlem12  30212  prtlem13  30213  prtlem15  30220  prtlem17  30221  prtlem18  30222  prter1  30224  prter3  30227  ismrcd1  30234  dford3lem2  30573  dford4  30575  pw2f1ocnv  30583  pw2f1o2  30584  wepwsolem  30591  fnwe2lem2  30601  aomclem8  30611  kelac1  30613  pwslnm  30644  idomsubgmo  30760  usgfis  31915  dflinc2  32084  lcosslsp  32112  sbcoreleleq  32385  tratrb  32386  ordelordALT  32388  trsbc  32391  truniALT  32392  onfrALTlem5  32394  onfrALTlem4  32395  onfrALTlem3  32396  onfrALTlem2  32398  onfrALTlem1  32400  onfrALT  32401  sspwtrALT  32700  suctrALT2  32717  tratrbVD  32741  truniALTVD  32758  trintALT  32761  onfrALTlem4VD  32766  bnj219  32868  bnj1098  32921  bnj594  33049  bnj580  33050  bnj601  33057  bnj849  33062  bnj996  33092  bnj1006  33096  bnj1029  33103  bnj1033  33104  bnj1090  33114  bnj1110  33117  bnj1124  33123  bnj1128  33125  bj-elequ2g  33319  bj-ax89  33320  bj-elequ12  33321  bj-cleljust  33425  bj-axext3  33435  bj-axext4  33436  bj-clabel  33450  bj-axrep1  33455  bj-axrep2  33456  bj-axrep3  33457  bj-axrep4  33458  bj-axrep5  33459  bj-axsep  33460  bj-nalset  33461  bj-zfpow  33462  bj-el  33463  bj-dtru  33464  bj-dvdemo1  33469  bj-dvdemo2  33470  bj-ax9  33545  bj-dfcleq  33547  bj-axsep2  33574  bj-ru0  33581  bj-ru1  33582  bj-ru  33583  bj-nul  33666  bj-nuliota  33667  bj-nuliotaALT  33668  pclfinclN  34746  dvh1dim  36239
  Copyright terms: Public domain W3C validator