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

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

Ref Expression
wel wff x y

Proof of Theorem wel
StepHypRef Expression
1 wcel 1380 1 wff x y
Colors of variables: wff set class
Syntax hints:   wcel 1380
This theorem is referenced by:  elequ1  1588  elequ2  1589  cleljust  1799  elsb3  1838  elsb4  1839  dveel1  1882  dveel2  1883  axext3  2009  axext4  2010  bm1.1  2011  ru  2742  nfuni  3562  nfunid  3563  unieq  3565  inteq  3594  nfint  3601  uniiun  3686  intiin  3687  trint  3845  axsep2  3852  bm1.3ii  3854  zfnuleu  3857  0ex  3860  nalset  3863  repizf2  3891  axpweq  3900  zfpow  3904  axpow2  3905  axpow3  3906  el  3907  dtruarb  3918  zfun  4121  axun2  4122  uniuni  4133  regexmid  4203  nnregexmid  4269  rele  4393  funimaexglem  4908  acexmidlem2  5433  acexmid  5435  dfsmo2  5821  smores2  5828  ltsopi  6167  bdcuni  6362  bdcint  6363  bdsep2  6368  bdsepnft  6369  bdsepnf  6370  bdsepnfALT  6371  bdzfauscl  6372  bdbm1.3ii  6373  bdinex1  6374  bj-zfpair2  6380  bj-axun2  6385  bj-uniex2  6386  strcoll2  6395  strcollnft  6396  strcollnf  6397  strcollnfALT  6398  sscoll2  6400
  Copyright terms: Public domain W3C validator