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

Theorem wel 1824
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 1824 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 1823. This lets us avoid overloading the  e. connective, thus preventing ambiguity that would complicate certain Metamath parsers. However, logically wel 1824 is considered to be a primitive syntax, even though here it is artificially "derived" from wcel 1823. 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 1823 1  wff  x  e.  y
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1823
This theorem is referenced by:  elequ1  1826  elequ2  1828  ax12wdemo  1836  cleljust  2111  cleljustALT  2112  dveel1  2113  dveel2  2114  axc14  2115  elsb3  2180  elsb4  2181  ax5el  2269  dveel2ALT  2271  ax12el  2274  axext2  2433  axext3  2434  axext3OLD  2435  axext4  2436  bm1.1  2437  bm1.1OLD  2438  sbabel  2647  ru  3323  nfuni  4241  nfunid  4242  unieq  4243  csbuni  4263  inteq  4274  nfint  4281  uniiun  4368  intiin  4369  trint  4547  trintss  4548  axrep1  4551  axrep2  4552  axrep3  4553  axrep4  4554  axrep5  4555  zfrepclf  4556  axsep  4559  axsep2  4561  bm1.3ii  4563  zfnuleu  4565  0ex  4569  nalset  4574  axpweq  4614  zfpow  4616  axpow2  4617  axpow3  4618  el  4619  dtru  4628  nfnid  4666  dvdemo1  4672  dvdemo2  4673  dfepfr  4853  wetrep  4861  wefrc  4862  ordelord  4889  rele  5120  funimaexg  5647  zfun  6566  axun2  6567  uniuni  6582  onint  6603  ordom  6682  dfsmo2  7010  smores2  7017  smo11  7027  smogt  7030  tz7.48lem  7098  tz7.48-2  7099  omeulem1  7223  pw2eng  7616  infensuc  7688  1sdom  7715  unxpdomlem1  7717  unxpdomlem2  7718  unxpdomlem3  7719  pssnn  7731  findcard2  7752  findcard2d  7754  ac6sfi  7756  frfi  7757  fissuni  7817  axreg2  8011  zfregcl  8012  dford2  8028  inf0  8029  inf1  8030  inf2  8031  zfinf  8047  axinf2  8048  zfinf2  8050  dfom4  8057  dfom5  8058  unbnn3  8066  noinfep  8067  cantnf  8103  cantnfOLD  8125  epfrs  8153  r111  8184  dif1card  8379  alephle  8460  aceq1  8489  aceq0  8490  aceq2  8491  dfac3  8493  dfac5lem2  8496  dfac5lem4  8498  dfac5  8500  dfac2a  8501  dfac2  8502  dfac7  8503  dfac0  8504  dfac1  8505  kmlem3  8523  kmlem4  8524  kmlem5  8525  kmlem8  8528  kmlem14  8534  kmlem15  8535  dfackm  8537  ackbij1lem10  8600  coflim  8632  cflim2  8634  cfsmolem  8641  fin23lem26  8696  ituniiun  8793  domtriomlem  8813  axdc3lem2  8822  zfac  8831  ac2  8832  ac3  8833  axac3  8835  axac2  8837  axac  8838  nd1  8953  nd2  8954  nd3  8955  nd4  8956  axextnd  8957  axrepndlem1  8958  axrepndlem2  8959  axrepnd  8960  axunndlem1  8961  axunnd  8962  axpowndlem1  8963  axpowndlem2  8964  axpowndlem3  8965  axpowndlem4  8966  axpownd  8967  axregndlem1  8968  axregndlem2  8969  axregnd  8970  axregndOLD  8971  axinfndlem1  8972  axinfnd  8973  axacndlem1  8974  axacndlem2  8975  axacndlem3  8976  axacndlem4  8977  axacndlem5  8978  axacnd  8979  fpwwe2lem12  9008  axgroth5  9191  axgroth2  9192  grothpw  9193  axgroth6  9195  grothomex  9196  axgroth3  9198  axgroth4  9199  grothprimlem  9200  grothprim  9201  nqereu  9296  npex  9353  elnpi  9355  hashbclem  12485  brfi1uzind  12516  fsum2dlem  13667  fprod2dlem  13866  fprod2d  13867  rpnnen  14044  ismre  15079  fnmre  15080  mremre  15093  isacs  15140  isacs1i  15146  mreacs  15147  acsfn1  15150  acsfn2  15152  isacs3lem  15995  pmtrprfval  16711  pmtrsn  16743  gsum2dlem2  17194  gsum2dOLD  17196  lbsextlem4  18002  drngnidl  18072  mplcoe1  18322  mplcoe5  18326  mplcoe2OLD  18328  zringlpir  18700  mdetunilem9  19289  mdetuni0  19290  maducoeval2  19309  madugsum  19312  isbasis3g  19617  tgcl  19638  tgss2  19656  toponmre  19761  neiptopnei  19800  ist0  19988  ishaus  19990  t0top  19997  haustop  19999  isreg  20000  ist0-2  20012  ist0-3  20013  t1t0  20016  ist1-3  20017  ishaus2  20019  haust1  20020  cmpsublem  20066  cmpsub  20067  tgcmp  20068  hauscmp  20074  bwth  20077  is1stc2  20109  2ndcctbss  20122  2ndcdisj  20123  2ndcdisj2  20124  2ndcomap  20125  2ndcsep  20126  dis2ndc  20127  restnlly  20149  restlly  20150  llyidm  20155  nllyidm  20156  lly1stc  20163  finptfin  20185  locfincmp  20193  ptpjopn  20279  tx1stc  20317  txkgen  20319  xkohaus  20320  xkococnlem  20326  xkoinjcn  20354  ist0-4  20396  kqt0lem  20403  regr1lem2  20407  kqt0  20413  r0sep  20415  nrmr0reg  20416  regr1  20417  kqreg  20418  kqnrm  20419  kqhmph  20486  filuni  20552  uffinfix  20594  fmfnfmlem4  20624  hauspwpwf1  20654  alexsublem  20710  alexsubALTlem3  20715  alexsubALTlem4  20716  alexsubALT  20717  blbas  21099  met1stc  21190  metrest  21193  xrsmopn  21483  cnheibor  21621  jensen  23516  sqff1o  23654  usgrafis  24617  cusgrasize  24680  dfconngra1  24873  0egra0rgra  25138  isplig  25381  tncp  25382  spanuni  26660  sumdmdii  27532  gsumvsca2  28009  indf1o  28253  gsumesum  28288  dya2iocuni  28491  erdsze  28910  conpcon  28944  rellyscon  28960  cvmsss2  28983  cvmlift2lem12  29023  axextprim  29314  axrepprim  29315  axunprim  29316  axpowprim  29317  axregprim  29318  axinfprim  29319  axacprim  29320  untelirr  29321  untuni  29322  untsucf  29323  unt0  29324  untint  29325  untangtr  29327  dftr6  29420  dffr5  29423  elpotr  29453  dfon2lem3  29457  dfon2lem4  29458  dfon2lem5  29459  dfon2lem6  29460  dfon2lem7  29461  dfon2lem8  29462  dfon2lem9  29463  dfon2  29464  domep  29465  axextdfeq  29470  ax8dfeq  29471  axextdist  29472  axext4dist  29473  exnel  29475  distel  29476  axextndbi  29477  poseq  29573  wfrlem12  29594  frrlem11  29639  nobndlem6  29697  nofulllem5  29706  dfiota3  29801  brcup  29817  brcap  29818  tfrqfree  29829  dfint3  29830  imagesset  29831  hftr  30067  onsuct0  30134  finixpnum  30278  fin2solem  30279  fin2so  30280  heicant  30289  mblfinlem1  30291  mbfresfi  30301  cnambfre  30303  ftc1anc  30338  ftc2nc  30339  fness  30407  fneref  30408  neibastop2lem  30418  cover2g  30445  sstotbnd2  30510  unichnidl  30668  prtlem5  30837  prtlem12  30848  prtlem13  30849  prtlem15  30856  prtlem17  30857  prtlem18  30858  prter1  30860  prter3  30863  ismrcd1  30870  dford3lem2  31208  dford4  31210  pw2f1ocnv  31218  pw2f1o2  31219  wepwsolem  31226  fnwe2lem2  31236  aomclem8  31246  kelac1  31248  pwslnm  31279  idomsubgmo  31396  usgfis  32818  dflinc2  33265  lcosslsp  33293  sbcoreleleq  33696  tratrb  33697  ordelordALT  33698  trsbc  33701  truniALT  33702  onfrALTlem5  33708  onfrALTlem4  33709  onfrALTlem3  33710  onfrALTlem2  33712  onfrALTlem1  33714  onfrALT  33715  sspwtrALT  34014  suctrALT2  34037  tratrbVD  34062  truniALTVD  34079  trintALT  34082  onfrALTlem4VD  34087  bnj219  34189  bnj1098  34243  bnj594  34371  bnj580  34372  bnj601  34379  bnj849  34384  bnj996  34414  bnj1006  34418  bnj1029  34425  bnj1033  34426  bnj1090  34436  bnj1110  34439  bnj1124  34445  bnj1128  34447  bj-elequ2g  34638  bj-ax89  34639  bj-elequ12  34640  bj-cleljust  34745  bj-axext3  34755  bj-axext4  34756  bj-clabel  34770  bj-axrep1  34775  bj-axrep2  34776  bj-axrep3  34777  bj-axrep4  34778  bj-axrep5  34779  bj-axsep  34780  bj-nalset  34781  bj-zfpow  34782  bj-el  34783  bj-dtru  34784  bj-dvdemo1  34789  bj-dvdemo2  34790  bj-ax9  34865  bj-dfcleq  34867  bj-axsep2  34894  bj-ru0  34901  bj-ru1  34902  bj-ru  34903  bj-nul  34986  bj-nuliota  34987  bj-nuliotaALT  34988  pclfinclN  36071  dvh1dim  37566  elintima  38177  lem1frege76a  38417
  Copyright terms: Public domain W3C validator