NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  wel Unicode version

Theorem wel 1401
Description: Extend wff definition to include atomic formulas with the epsilon (membership) predicate. This is read " is an element of ," " is a member of ," " belongs to ," or " contains ." Note: The phrase " includes " means " is a subset of ;" to use it also for , 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 (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 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 1401 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 1400. This lets us avoid overloading the connective, thus preventing ambiguity that would complicate certain Metamath parsers. However, logically wel 1401 is considered to be a primitive syntax, even though here it is artificially "derived" from wcel 1400. Note: To see the proof steps of this syntax proof, type "show proof wel /all" in the Metamath program.)

Assertion
Ref Expression
wel

Proof of Theorem wel
StepHypRef Expression
1 wcel 1400 1
Colors of variables: wff set class
Syntax hints:   wcel 1400
This theorem is referenced by:  elequ1  1534  elequ2  1535  cleljust  1732  elsb3  1735  elsb4  1736  dveel1  1765  dveel2  1766  ax15  1768  ax17el  1770  dveel2ALT  1771  ax11el  1773  csbing  2725  csbunig  3045  unipr  3051  uni0b  3060  uni0c  3061  csbifg  3134  axprimlem1  3190  axprimlem2  3191  axxpprim  3192  axcnvprim  3193  axssetprim  3194  axsiprim  3195  axtyplowerprim  3196  axins2prim  3197  axins3prim  3198  ninexg  3199  snex  3213  pwadjoin  3221  1cex  3246  xpkvexg  3389  p6exg  3394  ssetkex  3398  dfuni3  3419  dfint3  3422  unipw1  3435  dfpw2  3437  eqpw1uni  3440  dfaddc2  3489  dfnnc2  3503  peano2  3511  elsuc  3520  nnsucelrlem1  3531  nnsucelr  3535  nndisjeq  3536  prepeano4  3558  ltfinex  3572  ssfin  3578  ncfinraiselem2  3588  ncfinraise  3589  ncfinlowerlem1  3590  ncfinlower  3591  eqtfinrelk  3594  tfin11  3601  tfinsuc  3606  evenfinex  3611  oddfinex  3612  evenodddisjlem1  3623  nnadjoinlem1  3627  nnadjoin  3628  nnpweqlem1  3630  nnpweq  3631  srelk  3632  sfin112  3637  sfindbl  3638  tfinnnlem1  3641  tfinnn  3642  sfinltfin  3643  spfinex  3645  ncvspfin  3646  spfinsfincl  3647  spfininduct  3648  vfinspsslem1  3658  nulnnn  3664  dfop2lem1  3681  hbop  3710  sbcbrg  3782  setconslem2  3830  dfswap2  3839  epelc  3937  hbima  4145  csbima12g  4147  hbfv  4550  csbfv12g  4553  fv3  4558  tz6.12-1  4561  tz6.12-2  4564  fvopab4gf  4608  fvopabgf  4614  fvopabnf  4615  funiunfv  4707  csbovg  4789  ov2gf  4837  releqel  5028  releqmpt2  5032  cupex  5039  disjex  5042  addcfnex  5043  epprc  5046  crossex  5067  pw1fnex  5069  clos1conn  5092  dfnnc3  5097  transex  5121  refex  5122  antisymex  5123  connexex  5124  foundex  5125  extex  5126  symex  5127  qsexg  5194  enpw1  5274  enmap2lem1  5275  enmap1lem1  5281  enprmaplem1  5288  enprmaplem4  5291  enprmaplem5  5292  enprmaplem6  5293  nenpw1pwlem1  5296  lecex  5328  mucex  5346  peano4nc  5363  ncssfin  5364  nntccl  5383  ovcelem1  5384  ceexlem1  5386  nc0le1  5429  tcfnex  5456  nmembers1lem1  5464  nchoicelem10  5490  nchoicelem11  5491  nchoicelem16  5496  eq0cprim  5501  elsucprim  5502  eqsucprim  5503  elnncprim  5504  elphiprim  5505  elopprim  5506
  Copyright terms: Public domain W3C validator