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

Theorem wel 1375
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 1375 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 1374. This lets us avoid overloading the connective, thus preventing ambiguity that would complicate certain Metamath parsers. However, logically wel 1375 is considered to be a primitive syntax, even though here it is artificially "derived" from wcel 1374. 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 1374 1 wff x y
Colors of variables: wff set class
Syntax hints:   wcel 1374
This theorem is referenced by:  elequ1  1582  elequ2  1583  cleljust  1795  elsb3  1834  elsb4  1835  dveel1  1878  dveel2  1879  axext3  2005  axext4  2006  bm1.1  2007  ru  2740  nfuni  3560  nfunid  3561  unieq  3563  inteq  3592  nfint  3599  uniiun  3684  intiin  3685  trint  3843  axsep2  3850  bm1.3ii  3852  zfnuleu  3855  0ex  3858  nalset  3861  repizf2  3889  axpweq  3898  zfpow  3902  axpow2  3903  axpow3  3904  el  3905  dtruarb  3916  zfun  4121  axun2  4122  uniuni  4133  regexmid  4203  nnregexmid  4269  rele  4393  funimaexglem  4908  acexmidlem2  5433  acexmid  5435  dfsmo2  5824  smores2  5831  ltsopi  6180  bdcuni  7103  bdcint  7104  bdcriota  7110  bdsep2  7112  bdsepnft  7113  bdsepnf  7114  bdsepnfALT  7115  bdzfauscl  7116  bdbm1.3ii  7117  bj-nalset  7118  bdinex1  7122  bj-zfpair2  7133  bj-axun2  7138  bj-uniex2  7139  bj-nn0suc0  7172  bj-nntrans  7173  bj-omex2  7195  strcoll2  7201  strcollnft  7202  strcollnf  7203  strcollnfALT  7204  sscoll2  7206
  Copyright terms: Public domain W3C validator