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

Theorem wel 1888
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 syntactic 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 1888 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 1887. This lets us avoid overloading the  e. connective, thus preventing ambiguity that would complicate certain Metamath parsers. However, logically wel 1888 is considered to be a primitive syntax, even though here it is artificially "derived" from wcel 1887. 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 1887 1  wff  x  e.  y
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1887
This theorem is referenced by:  ax8  1893  elequ1  1894  cleljust  1895  ax9  1900  elequ2  1901  ax12wdemo  1909  cleljustALT  2089  cleljustALT2  2090  dveel1  2199  dveel2  2200  axc14  2201  elsb3  2263  elsb4  2264  axext2  2432  axext3  2433  axext3ALT  2434  axext4  2435  bm1.1  2436  sbabel  2620  ru  3266  nfuni  4204  nfunid  4205  unieq  4206  csbuni  4226  inteq  4237  nfint  4244  uniiun  4331  intiin  4332  trint  4512  trintss  4513  axrep1  4516  axrep2  4517  axrep3  4518  axrep4  4519  axrep5  4520  zfrepclf  4521  axsep  4524  axsep2  4526  bm1.3ii  4528  zfnuleu  4530  axnul  4532  0ex  4535  nalset  4540  axpweq  4580  zfpow  4582  axpow2  4583  axpow3  4584  el  4585  dtru  4594  nfnid  4629  dvdemo1  4635  dvdemo2  4636  dfepfr  4819  wetrep  4827  wefrc  4828  rele  4963  ordelord  5445  funimaexg  5660  zfun  6584  axun2  6585  uniuni  6600  onint  6622  ordom  6701  wfrlem12  7047  dfsmo2  7066  smores2  7073  smo11  7083  smogt  7086  dfrecs3  7091  tz7.48lem  7158  tz7.48-2  7159  omeulem1  7283  pw2eng  7678  infensuc  7750  1sdom  7775  unxpdomlem1  7776  unxpdomlem2  7777  unxpdomlem3  7778  pssnn  7790  findcard2  7811  findcard2d  7813  ac6sfi  7815  frfi  7816  fissuni  7879  axreg2  8108  zfregcl  8109  dford2  8125  inf0  8126  inf1  8127  inf2  8128  zfinf  8144  axinf2  8145  zfinf2  8147  dfom4  8154  dfom5  8155  unbnn3  8164  noinfep  8165  cantnf  8198  epfrs  8215  r111  8246  dif1card  8441  alephle  8519  aceq1  8548  aceq0  8549  aceq2  8550  dfac3  8552  dfac5lem2  8555  dfac5lem4  8557  dfac5  8559  dfac2a  8560  dfac2  8561  dfac7  8562  dfac0  8563  dfac1  8564  kmlem3  8582  kmlem4  8583  kmlem5  8584  kmlem8  8587  kmlem14  8593  kmlem15  8594  dfackm  8596  ackbij1lem10  8659  coflim  8691  cflim2  8693  cfsmolem  8700  fin23lem26  8755  ituniiun  8852  domtriomlem  8872  axdc3lem2  8881  zfac  8890  ac2  8891  ac3  8892  axac3  8894  axac2  8896  axac  8897  nd1  9012  nd2  9013  nd3  9014  nd4  9015  axextnd  9016  axrepndlem1  9017  axrepndlem2  9018  axrepnd  9019  axunndlem1  9020  axunnd  9021  axpowndlem1  9022  axpowndlem2  9023  axpowndlem3  9024  axpowndlem4  9025  axpownd  9026  axregndlem1  9027  axregndlem2  9028  axregnd  9029  axinfndlem1  9030  axinfnd  9031  axacndlem1  9032  axacndlem2  9033  axacndlem3  9034  axacndlem4  9035  axacndlem5  9036  axacnd  9037  fpwwe2lem12  9066  axgroth5  9249  axgroth2  9250  grothpw  9251  axgroth6  9253  grothomex  9254  axgroth3  9256  axgroth4  9257  grothprimlem  9258  grothprim  9259  nqereu  9354  npex  9411  elnpi  9413  hashbclem  12615  brfi1uzind  12651  brfi1indALT  12653  opfi1uzind  12654  fsum2dlem  13831  fprod2dlem  14034  fprod2d  14035  rpnnen  14279  lcmfunsnlem2lem2  14612  ismre  15496  fnmre  15497  mremre  15510  isacs  15557  isacs1i  15563  mreacs  15564  acsfn1  15567  acsfn2  15569  isacs3lem  16412  pmtrprfval  17128  pmtrsn  17160  gsum2dlem2  17603  lbsextlem4  18384  drngnidl  18453  mplcoe1  18689  mplcoe5  18692  zringlpirOLD  19059  mdetunilem9  19645  mdetuni0  19646  maducoeval2  19665  madugsum  19668  isbasis3g  19964  tgcl  19985  tgss2  20003  toponmre  20109  neiptopnei  20148  ist0  20336  ishaus  20338  t0top  20345  haustop  20347  isreg  20348  ist0-2  20360  ist0-3  20361  t1t0  20364  ist1-3  20365  ishaus2  20367  haust1  20368  cmpsublem  20414  cmpsub  20415  tgcmp  20416  hauscmp  20422  bwth  20425  is1stc2  20457  2ndcctbss  20470  2ndcdisj  20471  2ndcdisj2  20472  2ndcomap  20473  2ndcsep  20474  dis2ndc  20475  restnlly  20497  restlly  20498  llyidm  20503  nllyidm  20504  lly1stc  20511  finptfin  20533  locfincmp  20541  ptpjopn  20627  tx1stc  20665  txkgen  20667  xkohaus  20668  xkococnlem  20674  xkoinjcn  20702  ist0-4  20744  kqt0lem  20751  regr1lem2  20755  kqt0  20761  r0sep  20763  nrmr0reg  20764  regr1  20765  kqreg  20766  kqnrm  20767  kqhmph  20834  filuni  20900  uffinfix  20942  fmfnfmlem4  20972  hauspwpwf1  21002  alexsublem  21059  alexsubALTlem3  21064  alexsubALTlem4  21065  alexsubALT  21066  blbas  21445  met1stc  21536  metrest  21539  xrsmopn  21830  cnheibor  21983  jensen  23914  sqff1o  24109  usgrafis  25143  cusgrasize  25206  dfconngra1  25399  0egra0rgra  25664  isplig  25909  tncp  25910  spanuni  27197  sumdmdii  28068  gsumvsca2  28546  indf1o  28845  gsumesum  28880  dya2iocuni  29105  bnj219  29541  bnj1098  29595  bnj594  29723  bnj580  29724  bnj601  29731  bnj849  29736  bnj996  29766  bnj1006  29770  bnj1029  29777  bnj1033  29778  bnj1090  29788  bnj1110  29791  bnj1124  29797  bnj1128  29799  erdsze  29925  conpcon  29958  rellyscon  29974  cvmsss2  29997  cvmlift2lem12  30037  axextprim  30328  axrepprim  30329  axunprim  30330  axpowprim  30331  axregprim  30332  axinfprim  30333  axacprim  30334  untelirr  30335  untuni  30336  untsucf  30337  unt0  30338  untint  30339  untangtr  30341  dftr6  30390  dffr5  30393  elpotr  30427  dfon2lem3  30431  dfon2lem4  30432  dfon2lem5  30433  dfon2lem6  30434  dfon2lem7  30435  dfon2lem8  30436  dfon2lem9  30437  dfon2  30438  domep  30439  axextdfeq  30444  ax8dfeq  30445  axextdist  30446  axext4dist  30447  exnel  30449  distel  30450  axextndbi  30451  poseq  30491  frrlem11  30526  nobndlem6  30586  nofulllem5  30595  dfiota3  30690  brcup  30706  brcap  30707  dfint3  30719  imagesset  30720  hftr  30949  fness  31005  fneref  31006  neibastop2lem  31016  onsuct0  31101  bj-elequ2g  31275  bj-ax89  31276  bj-elequ12  31277  bj-cleljusti  31278  bj-axext3  31384  bj-axext4  31385  bj-clabel  31398  bj-axrep1  31403  bj-axrep2  31404  bj-axrep3  31405  bj-axrep4  31406  bj-axrep5  31407  bj-axsep  31408  bj-nalset  31409  bj-zfpow  31410  bj-el  31411  bj-dtru  31412  bj-dvdemo1  31417  bj-dvdemo2  31418  bj-ax8  31495  bj-ax9  31498  bj-cleqhyp  31499  bj-axsep2  31528  bj-ru0  31537  bj-ru1  31538  bj-ru  31539  bj-nul  31622  bj-nuliota  31623  bj-nuliotaALT  31624  finixpnum  31930  fin2solem  31931  fin2so  31932  poimirlem30  31970  poimirlem32  31972  poimir  31973  mblfinlem1  31977  mbfresfi  31987  cnambfre  31989  ftc1anc  32025  ftc2nc  32026  cover2g  32041  sstotbnd2  32106  unichnidl  32264  prtlem5  32430  prtlem12  32439  prtlem13  32440  prtlem15  32447  prtlem17  32448  prtlem18  32449  prter1  32451  prter3  32454  ax5el  32508  dveel2ALT  32510  ax12el  32513  pclfinclN  33515  dvh1dim  35010  ismrcd1  35540  dford3lem2  35882  dford4  35884  pw2f1ocnv  35892  pw2f1o2  35893  wepwsolem  35900  fnwe2lem2  35909  aomclem8  35919  kelac1  35921  pwslnm  35952  idomsubgmo  36072  inintabss  36184  inintabd  36185  cnvcnvintabd  36206  intabssd  36216  elintima  36245  dffrege76  36535  frege77  36536  frege89  36548  frege90  36549  frege91  36550  frege93  36552  frege94  36553  frege95  36554  sbcoreleleq  36896  tratrb  36897  ordelordALT  36898  trsbc  36901  truniALT  36902  onfrALTlem5  36908  onfrALTlem4  36909  onfrALTlem3  36910  onfrALTlem2  36912  onfrALTlem1  36914  onfrALT  36915  sspwtrALT  37210  suctrALT2  37233  tratrbVD  37258  truniALTVD  37275  trintALT  37278  onfrALTlem4VD  37283  uhgrnbgr0nb  39422  rusgrpropedg  39600  usgfis  39811  dflinc2  40256  lcosslsp  40284
  Copyright terms: Public domain W3C validator