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

Theorem wel 1697
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 1697 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 1696. This lets us avoid overloading the  e. connective, thus preventing ambiguity that would complicate certain Metamath parsers. However, logically wel 1697 is considered to be a primitive syntax, even though here it is artificially "derived" from wcel 1696. 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 1696 1  wff  x  e.  y
Colors of variables: wff set class
Syntax hints:    e. wcel 1696
This theorem is referenced by:  elequ1  1699  elequ2  1701  ax11wdemo  1709  cleljust  1967  cleljustALT  1968  dveel1  1972  dveel2  1973  ax15  1974  elsb3  2055  elsb4  2056  ax17el  2141  dveel2ALT  2143  ax11el  2146  trint  4144  trintss  4145  dfsmo2  6380  smores2  6387  smo11  6397  smogt  6400  tz7.48-2  6470  omeulem1  6596  infensuc  7055  unxpdomlem1  7083  findcard2  7114  ac6sfi  7117  fissuni  7176  dfom5  7367  noinfep  7376  epfrs  7429  r111  7463  dif1card  7654  alephle  7731  ackbij1lem10  7871  coflim  7903  fin23lem26  7967  ituniiun  8064  axac3  8106  axac2  8109  axac  8110  grothomex  8467  elnpi  8628  ismre  13508  fnmre  13509  mremre  13522  isacs  13569  isacs1i  13575  mreacs  13576  acsfn1  13579  acsfn2  13581  isacs3lem  14285  gsumdixp  15408  drngnidl  15997  zlpir  16460  2ndcdisj  17198  2ndcdisj2  17199  spanuni  22139  sumdmdii  23011  axextprim  24062  axrepprim  24063  axunprim  24064  axpowprim  24065  axregprim  24066  axinfprim  24067  axacprim  24068  untelirr  24069  untuni  24070  unt0  24072  untint  24073  untangtr  24075  dftr6  24177  dffr5  24180  elpotr  24207  dfon2lem4  24212  dfon2lem5  24213  dfon2lem6  24214  dfon2lem9  24217  dfon2  24218  axextdfeq  24224  ax13dfeq  24225  poseq  24323  wfrlem12  24337  tfrALTlem  24346  frrlem11  24363  nobndlem6  24421  nofulllem5  24430  dfiota3  24532  tfrqfree  24560  hftr  24883  onsuct0  24951  morcatset1  26017  pgapspf2  26155  isig1a2  26165  isig22  26167  elhaltdp  26169  tethpnc  26172  tpne  26177  linevala2  26180  ismrcd1  26875  dford3lem2  27222  fnwe2lem2  27250  kelac1  27263  pwslnm  27298  idomsubgmo  27616  sbcoreleleq  28596  tratrb  28597  ordelordALT  28599  trsbc  28602  truniALT  28603  onfrALTlem5  28605  onfrALTlem4  28606  onfrALTlem3  28607  onfrALTlem2  28609  onfrALTlem1  28611  onfrALT  28612  sspwtrALT  28911  pwtrOLD  28914  pwtrrOLD  28916  suctrALT2  28928  tratrbVD  28952  truniALTVD  28969  trintALT  28972  onfrALTlem4VD  28977  bnj594  29259  bnj580  29260  bnj601  29267  bnj849  29272  bnj1029  29313  bnj1090  29324  bnj1110  29327  bnj1124  29333  bnj1128  29335  dveel1NEW7  29441  dveel2NEW7  29442  ax15NEW7  29510  elsb3NEW7  29574  elsb4NEW7  29575  cleljustNEW7  29598  cleljustALTNEW7  29599  dvh1dim  32254
  Copyright terms: Public domain W3C validator