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

Theorem wel 1711
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 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

Proof of Theorem wel
StepHypRef Expression
1 wcel 1710 1
Colors of variables: wff set 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  4412  nnsucelrlem1  4423  nnsucelr  4427  nndisjeq  4428  prepeano4  4450  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  4724  dfswap2  4733  epelc  4757  tz6.12-2  5386  chfnrn  5439  funiunfv  5507  releqel  5837  releqmpt2  5841  cupex  5848  disjex  5851  addcfnex  5852  epprc  5855  crossex  5876  pw1fnex  5878  clos1conn  5901  dfnnc3  5906  transex  5930  refex  5931  antisymex  5932  connexex  5933  foundex  5934  extex  5935  symex  5936  qsexg  6002  enpw1  6082  enmap2lem1  6083  enmap1lem1  6089  enprmaplem1  6096  enprmaplem4  6099  enprmaplem5  6100  enprmaplem6  6101  nenpw1pwlem1  6104  lecex  6136  mucex  6154  peano4nc  6171  ncssfin  6172  nntccl  6191  ovcelem1  6192  ceexlem1  6194  nc0le1  6237  tcfnex  6264  nmembers1lem1  6272  nchoicelem10  6298  nchoicelem11  6299  nchoicelem16  6304
  Copyright terms: Public domain W3C validator