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

Theorem wel 1391
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 1391 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 1390. This lets us avoid overloading the connective, thus preventing ambiguity that would complicate certain Metamath parsers. However, logically wel 1391 is considered to be a primitive syntax, even though here it is artificially "derived" from wcel 1390. 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 1390 1
Colors of variables: wff set class
Syntax hints:   wcel 1390
This theorem is referenced by:  elequ1  1597  elequ2  1598  cleljust  1810  elsb3  1849  elsb4  1850  dveel1  1893  dveel2  1894  axext3  2020  axext4  2021  bm1.1  2022  ru  2757  nfuni  3577  nfunid  3578  unieq  3580  inteq  3609  nfint  3616  uniiun  3701  intiin  3702  trint  3860  axsep2  3867  bm1.3ii  3869  zfnuleu  3872  0ex  3875  nalset  3878  repizf2  3906  axpweq  3915  zfpow  3919  axpow2  3920  axpow3  3921  el  3922  dtruarb  3933  zfun  4137  axun2  4138  uniuni  4149  regexmid  4219  nnregexmid  4285  rele  4409  funimaexglem  4925  acexmidlem2  5452  acexmid  5454  dfsmo2  5843  smores2  5850  ltsopi  6304  bdcuni  9311  bdcint  9312  bdcriota  9318  bdsep2  9320  bdsepnft  9321  bdsepnf  9322  bdsepnfALT  9323  bdzfauscl  9324  bdbm1.3ii  9325  bj-nalset  9326  bdinex1  9330  bj-zfpair2  9341  bj-axun2  9346  bj-uniex2  9347  bj-d0clsepcl  9360  bj-nn0suc0  9384  bj-nntrans  9385  bj-omex2  9407  strcoll2  9413  strcollnft  9414  strcollnf  9415  strcollnfALT  9416  sscoll2  9418
  Copyright terms: Public domain W3C validator