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

Theorem wel 1685
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 1685 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 1684. This lets us avoid overloading the  e. connective, thus preventing ambiguity that would complicate certain Metamath parsers. However, logically wel 1685 is considered to be a primitive syntax, even though here it is artificially "derived" from wcel 1684. 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 1684 1  wff  x  e.  y
Colors of variables: wff set class
Syntax hints:    e. wcel 1684
This theorem is referenced by:  elequ1  1687  elequ2  1689  ax11wdemo  1697  cleljust  1954  cleljustALT  1955  dveel1  1959  dveel2  1960  ax15  1961  elsb3  2042  elsb4  2043  ax17el  2128  dveel2ALT  2130  ax11el  2133  trint  4128  trintss  4129  dfsmo2  6364  smores2  6371  smo11  6381  smogt  6384  tz7.48-2  6454  omeulem1  6580  infensuc  7039  unxpdomlem1  7067  findcard2  7098  ac6sfi  7101  fissuni  7160  dfom5  7351  noinfep  7360  epfrs  7413  r111  7447  dif1card  7638  alephle  7715  ackbij1lem10  7855  coflim  7887  fin23lem26  7951  ituniiun  8048  axac3  8090  axac2  8093  axac  8094  grothomex  8451  elnpi  8612  ismre  13492  fnmre  13493  mremre  13506  isacs  13553  isacs1i  13559  mreacs  13560  acsfn1  13563  acsfn2  13565  isacs3lem  14269  gsumdixp  15392  drngnidl  15981  zlpir  16444  2ndcdisj  17182  2ndcdisj2  17183  spanuni  22123  sumdmdii  22995  axextprim  23458  axrepprim  23459  axunprim  23460  axpowprim  23461  axregprim  23462  axinfprim  23463  axacprim  23464  untelirr  23465  untuni  23466  unt0  23468  untint  23469  untangtr  23471  dftr6  23518  dffr5  23521  elpotr  23548  dfon2lem4  23553  dfon2lem5  23554  dfon2lem6  23555  dfon2lem9  23558  dfon2  23559  axextdfeq  23565  ax13dfeq  23566  poseq  23664  wfrlem12  23678  tfrALTlem  23687  frrlem11  23704  nobndlem6  23762  nofulllem5  23771  dfiota3  23873  tfrqfree  23900  hftr  24223  onsuct0  24291  morcatset1  25327  pgapspf2  25465  isig1a2  25475  isig22  25477  elhaltdp  25479  tethpnc  25482  tpne  25487  linevala2  25490  ismrcd1  26185  dford3lem2  26532  fnwe2lem2  26560  kelac1  26573  pwslnm  26608  idomsubgmo  26926  sbcoreleleq  27671  tratrb  27672  ordelordALT  27674  trsbc  27677  truniALT  27678  onfrALTlem5  27680  onfrALTlem4  27681  onfrALTlem3  27682  onfrALTlem2  27684  onfrALTlem1  27686  onfrALT  27687  sspwtrALT  27969  pwtrOLD  27972  pwtrrOLD  27974  suctrALT2  27986  tratrbVD  28010  truniALTVD  28027  trintALT  28030  onfrALTlem4VD  28035  bnj594  28317  bnj580  28318  bnj601  28325  bnj849  28330  bnj1029  28371  bnj1090  28382  bnj1110  28385  bnj1124  28391  bnj1128  28393  dvh1dim  31005
  Copyright terms: Public domain W3C validator