Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  wel Unicode version

Theorem wel 1482
 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 1482 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 1481. This lets us avoid overloading the connective, thus preventing ambiguity that would complicate certain Metamath parsers. However, logically wel 1482 is considered to be a primitive syntax, even though here it is artificially "derived" from wcel 1481. 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 1481 1
 Colors of variables: wff set class Syntax hints:   wcel 1481 This theorem is referenced by:  elequ1  1691  elequ2  1692  cleljust  1911  elsb3  1952  elsb4  1953  dveel1  1996  dveel2  1997  axext3  2123  axext4  2124  bm1.1  2125  ru  2913  nfuni  3751  nfunid  3752  unieq  3754  inteq  3783  nfint  3790  uniiun  3875  intiin  3876  trint  4050  axsep2  4056  bm1.3ii  4058  zfnuleu  4061  0ex  4064  nalset  4067  vnex  4068  repizf2  4095  axpweq  4104  zfpow  4108  axpow2  4109  axpow3  4110  el  4111  vpwex  4112  dtruarb  4124  exmidn0m  4133  exmidsssn  4134  fr0  4282  wetrep  4291  zfun  4365  axun2  4366  uniuni  4381  regexmid  4459  zfregfr  4497  ordwe  4499  wessep  4501  nnregexmid  4543  rele  4678  funimaexglem  5215  acexmidlem2  5780  acexmid  5782  dfsmo2  6193  smores2  6200  tfrcllemsucaccv  6260  findcard2d  6794  exmidfodomr  7080  acfun  7083  onntri13  7109  onntri51  7110  ccfunen  7116  cc1  7117  ltsopi  7172  fnn0nninf  10261  fsum2dlemstep  11255  exmidunben  11995  isbasis3g  12272  tgcl  12292  tgss2  12307  blbas  12661  metrest  12734  bdcuni  13265  bdcint  13266  bdcriota  13272  bdsep1  13274  bdsep2  13275  bdsepnft  13276  bdsepnf  13277  bdsepnfALT  13278  bdzfauscl  13279  bdbm1.3ii  13280  bj-axemptylem  13281  bj-axempty  13282  bj-axempty2  13283  bj-nalset  13284  bdinex1  13288  bj-zfpair2  13299  bj-axun2  13304  bj-uniex2  13305  bj-d0clsepcl  13314  bj-nn0suc0  13339  bj-nntrans  13340  bj-omex2  13366  strcollnft  13373  sscoll2  13377  nninfsellemcl  13401  nninfsellemsuc  13402  nninfsellemqall  13405  nninfomni  13409  exmidsbthrlem  13411
 Copyright terms: Public domain W3C validator