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

Theorem wel 1726
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 1726 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 1725. This lets us avoid overloading the  e. connective, thus preventing ambiguity that would complicate certain Metamath parsers. However, logically wel 1726 is considered to be a primitive syntax, even though here it is artificially "derived" from wcel 1725. 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 1725 1  wff  x  e.  y
Colors of variables: wff set class
Syntax hints:    e. wcel 1725
This theorem is referenced by:  elequ1  1728  elequ2  1730  ax11wdemo  1738  cleljust  2103  cleljustALT  2104  dveel1  2105  dveel2  2106  ax15  2107  elsb3  2179  elsb4  2180  ax17el  2266  dveel2ALT  2268  ax11el  2271  axext2  2418  axext3  2419  axext4  2420  bm1.1  2421  ru  3160  nfuni  4021  nfunid  4022  unieq  4024  inteq  4053  nfint  4060  uniiun  4144  intiin  4145  trint  4317  trintss  4318  axrep1  4321  axrep2  4322  axrep3  4323  axrep4  4324  axrep5  4325  zfrepclf  4326  axsep  4329  axsep2  4331  bm1.3ii  4333  zfnuleu  4335  0ex  4339  nalset  4340  axpweq  4376  zfpow  4378  axpow2  4379  axpow3  4380  el  4381  dtru  4390  nfnid  4393  dvdemo1  4399  dvdemo2  4400  dfepfr  4567  wetrep  4575  wefrc  4576  ordelord  4603  zfun  4702  axun2  4703  uniuni  4716  onint  4775  ordom  4854  rele  5003  funimaexg  5530  dfsmo2  6609  smores2  6616  smo11  6626  smogt  6629  tz7.48lem  6698  tz7.48-2  6699  omeulem1  6825  pw2eng  7214  infensuc  7285  1sdom  7311  unxpdomlem1  7313  unxpdomlem2  7314  unxpdomlem3  7315  pssnn  7327  findcard2  7348  ac6sfi  7351  frfi  7352  fissuni  7411  axreg2  7561  zfregcl  7562  dford2  7575  inf0  7576  inf1  7577  inf2  7578  zfinf  7594  axinf2  7595  zfinf2  7597  dfom4  7604  dfom5  7605  unbnn3  7613  noinfep  7614  cantnf  7649  epfrs  7667  r111  7701  dif1card  7892  alephle  7969  aceq1  7998  aceq0  7999  aceq2  8000  dfac3  8002  dfac5lem2  8005  dfac5lem4  8007  dfac5  8009  dfac2a  8010  dfac2  8011  dfac7  8012  dfac0  8013  dfac1  8014  kmlem3  8032  kmlem4  8033  kmlem5  8034  kmlem8  8037  kmlem14  8043  kmlem15  8044  dfackm  8046  ackbij1lem10  8109  coflim  8141  cflim2  8143  cfsmolem  8150  fin23lem26  8205  ituniiun  8302  domtriomlem  8322  axdc3lem2  8331  zfac  8340  ac2  8341  ac3  8342  axac3  8344  axac2  8346  axac  8347  nd1  8462  nd2  8463  nd3  8464  nd4  8465  axextnd  8466  axrepndlem1  8467  axrepndlem2  8468  axrepnd  8469  axunndlem1  8470  axunnd  8471  axpowndlem1  8472  axpowndlem2  8473  axpowndlem4  8475  axpownd  8476  axregndlem1  8477  axregndlem2  8478  axregnd  8479  axinfndlem1  8480  axinfnd  8481  axacndlem1  8482  axacndlem2  8483  axacndlem3  8484  axacndlem4  8485  axacndlem5  8486  axacnd  8487  fpwwe2lem12  8516  axgroth5  8699  axgroth2  8700  grothpw  8701  axgroth6  8703  grothomex  8704  axgroth3  8706  axgroth4  8707  grothprimlem  8708  grothprim  8709  nqereu  8806  npex  8863  elnpi  8865  hashbclem  11701  brfi1uzind  11715  fsum2dlem  12554  rpnnen  12826  ismre  13815  fnmre  13816  mremre  13829  isacs  13876  isacs1i  13882  mreacs  13883  acsfn1  13886  acsfn2  13888  isacs3lem  14592  gsum2d  15546  lbsextlem4  16233  drngnidl  16300  mplcoe1  16528  mplcoe2  16530  zlpir  16771  isbasis3g  17014  tgcl  17034  tgss2  17052  toponmre  17157  neiptopnei  17196  ist0  17384  ishaus  17386  t0top  17393  haustop  17395  isreg  17396  ist0-2  17408  ist0-3  17409  t1t0  17412  ist1-3  17413  ishaus2  17415  haust1  17416  cmpsublem  17462  cmpsub  17463  tgcmp  17464  hauscmp  17470  is1stc2  17505  2ndcctbss  17518  2ndcdisj  17519  2ndcdisj2  17520  2ndcomap  17521  2ndcsep  17522  dis2ndc  17523  restnlly  17545  restlly  17546  llyidm  17551  nllyidm  17552  lly1stc  17559  ptpjopn  17644  tx1stc  17682  txkgen  17684  xkohaus  17685  xkococnlem  17691  xkoinjcn  17719  ist0-4  17761  kqt0lem  17768  regr1lem2  17772  kqt0  17778  r0sep  17780  nrmr0reg  17781  regr1  17782  kqreg  17783  kqnrm  17784  kqhmph  17851  filuni  17917  uffinfix  17959  fmfnfmlem4  17989  hauspwpwf1  18019  alexsublem  18075  alexsubALTlem3  18080  alexsubALTlem4  18081  alexsubALT  18082  blbas  18460  met1stc  18551  metrest  18554  xrsmopn  18843  cnheibor  18980  jensen  20827  sqff1o  20965  usgrafis  21429  cusgrasize  21487  dfconngra1  21658  isplig  21765  tncp  21766  spanuni  23046  sumdmdii  23918  indf1o  24421  gsumesum  24451  dya2iocuni  24633  erdsze  24888  conpcon  24922  rellyscon  24938  cvmsss2  24961  cvmlift2lem12  25001  axextprim  25150  axrepprim  25151  axunprim  25152  axpowprim  25153  axregprim  25154  axinfprim  25155  axacprim  25156  untelirr  25157  untuni  25158  untsucf  25159  unt0  25160  untint  25161  untangtr  25163  fprod2dlem  25304  fprod2d  25305  dftr6  25373  dffr5  25376  elpotr  25408  dfon2lem3  25412  dfon2lem4  25413  dfon2lem5  25414  dfon2lem6  25415  dfon2lem7  25416  dfon2lem8  25417  dfon2lem9  25418  dfon2  25419  domep  25420  axextdfeq  25425  ax13dfeq  25426  axextdist  25427  axext4dist  25428  exnel  25430  distel  25431  axextndbi  25432  poseq  25528  wfrlem12  25549  frrlem11  25594  nobndlem6  25652  nofulllem5  25661  dfiota3  25768  brcup  25784  brcap  25785  tfrqfree  25796  dfint3  25797  imagesset  25798  hftr  26123  onsuct0  26191  mblfinlem1  26243  mbfresfi  26253  cnambfre  26255  ftc1anc  26288  ftc2nc  26289  fness  26362  fneref  26364  fnessref  26373  finptfin  26377  locfincmp  26384  comppfsc  26387  neibastop2lem  26389  cover2g  26416  sstotbnd2  26483  unichnidl  26641  prtlem5  26705  prtlem12  26716  prtlem13  26717  prtlem15  26724  prtlem17  26725  prtlem18  26726  prter1  26728  prter3  26731  ismrcd1  26752  dford3lem2  27098  dford4  27100  pw2f1ocnv  27108  pw2f1o2  27109  wepwsolem  27116  fnwe2lem2  27126  aomclem8  27136  kelac1  27138  pwslnm  27173  idomsubgmo  27491  0egra0rgra  28375  sbcoreleleq  28619  tratrb  28620  ordelordALT  28622  trsbc  28625  truniALT  28626  onfrALTlem5  28628  onfrALTlem4  28629  onfrALTlem3  28630  onfrALTlem2  28632  onfrALTlem1  28634  onfrALT  28635  sspwtrALT  28935  suctrALT2  28949  tratrbVD  28973  truniALTVD  28990  trintALT  28993  onfrALTlem4VD  28998  bnj219  29100  bnj1098  29154  bnj594  29283  bnj580  29284  bnj601  29291  bnj849  29296  bnj996  29326  bnj1006  29330  bnj1029  29337  bnj1033  29338  bnj1090  29348  bnj1110  29351  bnj1124  29357  bnj1128  29359  dveel1NEW7  29465  dveel2NEW7  29466  ax15NEW7  29536  elsb3NEW7  29603  elsb4NEW7  29604  cleljustNEW7  29627  elsb34AUX7  29672  ax7w13AUX7  29673  pclfinclN  30747  dvh1dim  32240
  Copyright terms: Public domain W3C validator