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

Theorem wel 1722
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 1722 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 1721. This lets us avoid overloading the  e. connective, thus preventing ambiguity that would complicate certain Metamath parsers. However, logically wel 1722 is considered to be a primitive syntax, even though here it is artificially "derived" from wcel 1721. 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 1721 1  wff  x  e.  y
Colors of variables: wff set class
Syntax hints:    e. wcel 1721
This theorem is referenced by:  elequ1  1724  elequ2  1726  ax11wdemo  1734  cleljust  2064  cleljustALT  2065  dveel1  2068  dveel2  2069  ax15  2070  elsb3  2152  elsb4  2153  ax17el  2239  dveel2ALT  2241  ax11el  2244  axext2  2386  axext3  2387  axext4  2388  bm1.1  2389  ru  3120  nfuni  3981  nfunid  3982  unieq  3984  inteq  4013  nfint  4020  uniiun  4104  intiin  4105  trint  4277  trintss  4278  axrep1  4281  axrep2  4282  axrep3  4283  axrep4  4284  axrep5  4285  zfrepclf  4286  axsep  4289  axsep2  4291  bm1.3ii  4293  zfnuleu  4295  0ex  4299  nalset  4300  axpweq  4336  zfpow  4338  axpow2  4339  axpow3  4340  el  4341  dtru  4350  nfnid  4353  dvdemo1  4359  dvdemo2  4360  dfepfr  4527  wetrep  4535  wefrc  4536  ordelord  4563  zfun  4661  axun2  4662  uniuni  4675  onint  4734  ordom  4813  rele  4962  funimaexg  5489  dfsmo2  6568  smores2  6575  smo11  6585  smogt  6588  tz7.48lem  6657  tz7.48-2  6658  omeulem1  6784  pw2eng  7173  infensuc  7244  1sdom  7270  unxpdomlem1  7272  unxpdomlem2  7273  unxpdomlem3  7274  pssnn  7286  findcard2  7307  ac6sfi  7310  frfi  7311  fissuni  7369  axreg2  7517  zfregcl  7518  ruv  7524  dford2  7531  inf0  7532  inf1  7533  inf2  7534  zfinf  7550  axinf2  7551  zfinf2  7553  dfom4  7560  dfom5  7561  unbnn3  7569  noinfep  7570  cantnf  7605  epfrs  7623  r111  7657  dif1card  7848  alephle  7925  aceq1  7954  aceq0  7955  aceq2  7956  dfac3  7958  dfac5lem2  7961  dfac5lem4  7963  dfac5  7965  dfac2a  7966  dfac2  7967  dfac7  7968  dfac0  7969  dfac1  7970  kmlem3  7988  kmlem4  7989  kmlem5  7990  kmlem8  7993  kmlem14  7999  kmlem15  8000  dfackm  8002  ackbij1lem10  8065  coflim  8097  cflim2  8099  cfsmolem  8106  fin23lem26  8161  ituniiun  8258  domtriomlem  8278  axdc3lem2  8287  zfac  8296  ac2  8297  ac3  8298  axac3  8300  axac2  8302  axac  8303  nd1  8418  nd2  8419  nd3  8420  nd4  8421  axextnd  8422  axrepndlem1  8423  axrepndlem2  8424  axrepnd  8425  axunndlem1  8426  axunnd  8427  axpowndlem1  8428  axpowndlem2  8429  axpowndlem4  8431  axpownd  8432  axregndlem1  8433  axregndlem2  8434  axregnd  8435  axinfndlem1  8436  axinfnd  8437  axacndlem1  8438  axacndlem2  8439  axacndlem3  8440  axacndlem4  8441  axacndlem5  8442  axacnd  8443  fpwwe2lem12  8472  axgroth5  8655  axgroth2  8656  grothpw  8657  axgroth6  8659  grothomex  8660  axgroth3  8662  axgroth4  8663  grothprimlem  8664  grothprim  8665  nqereu  8762  npex  8819  elnpi  8821  hashbclem  11656  brfi1uzind  11670  fsum2dlem  12509  rpnnen  12781  ismre  13770  fnmre  13771  mremre  13784  isacs  13831  isacs1i  13837  mreacs  13838  acsfn1  13841  acsfn2  13843  isacs3lem  14547  gsum2d  15501  lbsextlem4  16188  drngnidl  16255  mplcoe1  16483  mplcoe2  16485  zlpir  16726  isbasis3g  16969  tgcl  16989  tgss2  17007  toponmre  17112  neiptopnei  17151  ist0  17338  ishaus  17340  t0top  17347  haustop  17349  isreg  17350  ist0-2  17362  ist0-3  17363  t1t0  17366  ist1-3  17367  ishaus2  17369  haust1  17370  cmpsublem  17416  cmpsub  17417  tgcmp  17418  hauscmp  17424  is1stc2  17458  2ndcctbss  17471  2ndcdisj  17472  2ndcdisj2  17473  2ndcomap  17474  2ndcsep  17475  dis2ndc  17476  restnlly  17498  restlly  17499  llyidm  17504  nllyidm  17505  lly1stc  17512  ptpjopn  17597  tx1stc  17635  txkgen  17637  xkohaus  17638  xkococnlem  17644  xkoinjcn  17672  ist0-4  17714  kqt0lem  17721  regr1lem2  17725  kqt0  17731  r0sep  17733  nrmr0reg  17734  regr1  17735  kqreg  17736  kqnrm  17737  kqhmph  17804  filuni  17870  uffinfix  17912  fmfnfmlem4  17942  hauspwpwf1  17972  alexsublem  18028  alexsubALTlem3  18033  alexsubALTlem4  18034  alexsubALT  18035  blbas  18413  met1stc  18504  metrest  18507  xrsmopn  18796  cnheibor  18933  jensen  20780  sqff1o  20918  usgrafis  21382  cusgrasize  21440  dfconngra1  21611  isplig  21718  tncp  21719  spanuni  22999  sumdmdii  23871  indf1o  24374  gsumesum  24404  dya2iocuni  24586  erdsze  24841  conpcon  24875  rellyscon  24891  cvmsss2  24914  cvmlift2lem12  24954  axextprim  25103  axrepprim  25104  axunprim  25105  axpowprim  25106  axregprim  25107  axinfprim  25108  axacprim  25109  untelirr  25110  untuni  25111  untsucf  25112  unt0  25113  untint  25114  untangtr  25116  fprod2dlem  25257  fprod2d  25258  dftr6  25321  dffr5  25324  elpotr  25351  dfon2lem3  25355  dfon2lem4  25356  dfon2lem5  25357  dfon2lem6  25358  dfon2lem7  25359  dfon2lem8  25360  dfon2lem9  25361  dfon2  25362  domep  25363  axextdfeq  25368  ax13dfeq  25369  axextdist  25370  axext4dist  25371  exnel  25373  distel  25374  axextndbi  25375  poseq  25467  wfrlem12  25481  tfrALTlem  25490  frrlem11  25507  nobndlem6  25565  nofulllem5  25574  dfiota3  25676  tfrqfree  25704  hftr  26027  onsuct0  26095  mblfinlem  26143  mbfresfi  26152  cnambfre  26154  fness  26252  fneref  26254  fnessref  26263  finptfin  26267  locfincmp  26274  comppfsc  26277  neibastop2lem  26279  cover2g  26306  sstotbnd2  26373  unichnidl  26531  prtlem5  26595  prtlem12  26606  prtlem13  26607  prtlem15  26614  prtlem17  26615  prtlem18  26616  prter1  26618  prter3  26621  ismrcd1  26642  dford3lem2  26988  dford4  26990  pw2f1ocnv  26998  pw2f1o2  26999  wepwsolem  27006  fnwe2lem2  27016  aomclem8  27027  kelac1  27029  pwslnm  27064  idomsubgmo  27382  sbcoreleleq  28330  tratrb  28331  ordelordALT  28333  trsbc  28336  truniALT  28337  onfrALTlem5  28339  onfrALTlem4  28340  onfrALTlem3  28341  onfrALTlem2  28343  onfrALTlem1  28345  onfrALT  28346  sspwtrALT  28644  suctrALT2  28658  tratrbVD  28682  truniALTVD  28699  trintALT  28702  onfrALTlem4VD  28707  bnj219  28806  bnj1098  28860  bnj594  28989  bnj580  28990  bnj601  28997  bnj849  29002  bnj996  29032  bnj1006  29036  bnj1029  29043  bnj1033  29044  bnj1090  29054  bnj1110  29057  bnj1124  29063  bnj1128  29065  dveel1NEW7  29171  dveel2NEW7  29172  ax15NEW7  29240  elsb3NEW7  29304  elsb4NEW7  29305  cleljustNEW7  29328  pclfinclN  30432  dvh1dim  31925
  Copyright terms: Public domain W3C validator