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  24178  dffr5  24181  elpotr  24208  dfon2lem4  24213  dfon2lem5  24214  dfon2lem6  24215  dfon2lem9  24218  dfon2  24219  axextdfeq  24225  ax13dfeq  24226  poseq  24324  wfrlem12  24338  tfrALTlem  24347  frrlem11  24364  nobndlem6  24422  nofulllem5  24431  dfiota3  24533  tfrqfree  24561  hftr  24884  onsuct0  24952  morcatset1  26018  pgapspf2  26156  isig1a2  26166  isig22  26168  elhaltdp  26170  tethpnc  26173  tpne  26178  linevala2  26181  ismrcd1  26876  dford3lem2  27223  fnwe2lem2  27251  kelac1  27264  pwslnm  27299  idomsubgmo  27617  sbcoreleleq  28597  tratrb  28598  ordelordALT  28600  trsbc  28603  truniALT  28604  onfrALTlem5  28606  onfrALTlem4  28607  onfrALTlem3  28608  onfrALTlem2  28610  onfrALTlem1  28612  onfrALT  28613  sspwtrALT  28912  pwtrOLD  28915  pwtrrOLD  28917  suctrALT2  28929  tratrbVD  28953  truniALTVD  28970  trintALT  28973  onfrALTlem4VD  28978  bnj594  29260  bnj580  29261  bnj601  29268  bnj849  29273  bnj1029  29314  bnj1090  29325  bnj1110  29328  bnj1124  29334  bnj1128  29336  dveel1NEW7  29442  dveel2NEW7  29443  ax15NEW7  29511  elsb3NEW7  29575  elsb4NEW7  29576  cleljustNEW7  29599  cleljustALTNEW7  29600  dvh1dim  32254
  Copyright terms: Public domain W3C validator