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

Theorem wel 1711
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 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 (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 1711 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 1710. This lets us avoid overloading the connective, thus preventing ambiguity that would complicate certain Metamath parsers. However, logically wel 1711 is considered to be a primitive syntax, even though here it is artificially "derived" from wcel 1710. 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 y

Proof of Theorem wel
StepHypRef Expression
1 wcel 1710 1 wff x y
Colors of variables: wff setvar class
Syntax hints:   wcel 1710
This theorem is referenced by:  elequ1  1713  elequ2  1715  ax11wdemo  1723  cleljust  2014  cleljustALT  2015  dveel1  2019  dveel2  2020  ax15  2021  elsb3  2103  elsb4  2104  ax17el  2189  dveel2ALT  2191  ax11el  2194  unipr  3905  iinuni  4049  axprimlem1  4088  axprimlem2  4089  axxpprim  4090  axcnvprim  4091  axssetprim  4092  axsiprim  4093  axtyplowerprim  4094  axins2prim  4095  axins3prim  4096  ninexg  4097  snex  4111  pwadjoin  4119  1cex  4142  xpkvexg  4285  p6exg  4290  ssetkex  4294  dfuni3  4315  dfint3  4318  unipw1  4325  dfpw2  4327  eqpw1uni  4330  dfaddc2  4381  dfnnc2  4395  peano2  4403  elsuc  4413  nnsucelrlem1  4424  nnsucelr  4428  nndisjeq  4429  prepeano4  4451  ltfinex  4464  ssfin  4470  ncfinraiselem2  4480  ncfinraise  4481  ncfinlowerlem1  4482  ncfinlower  4483  eqtfinrelk  4486  tfin11  4493  tfinsuc  4498  evenfinex  4503  oddfinex  4504  evenodddisjlem1  4515  nnadjoinlem1  4519  nnadjoin  4520  nnpweqlem1  4522  nnpweq  4523  srelk  4524  sfin112  4529  sfindbl  4530  tfinnnlem1  4533  tfinnn  4534  sfinltfin  4535  spfinex  4537  ncvspfin  4538  spfinsfincl  4539  spfininduct  4540  vfinspsslem1  4550  nulnnn  4556  dfop2lem1  4573  setconslem2  4732  dfswap2  4741  epelc  4765  tz6.12-2  5346  chfnrn  5399  funiunfv  5467  releqel  5807  releqmpt2  5809  cupex  5816  composeex  5820  disjex  5823  addcfnex  5824  epprc  5827  crossex  5850  pw1fnex  5852  domfnex  5870  ranfnex  5871  clos1conn  5879  dfnnc3  5885  transex  5910  refex  5911  antisymex  5912  connexex  5913  foundex  5914  extex  5915  symex  5916  qsexg  5982  enpw1  6062  enprmaplem1  6076  enprmaplem4  6079  enprmaplem5  6080  enprmaplem6  6081  nenpw1pwlem1  6084  lecex  6115  mucex  6133  peano4nc  6150  ncssfin  6151  nntccl  6170  ovcelem1  6171  ceexlem1  6173  nc0le1  6216  tcfnex  6244  nmembers1lem1  6268  nchoicelem10  6297  nchoicelem11  6298  nchoicelem16  6303
  Copyright terms: Public domain W3C validator