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

Theorem wel 1391
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 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.)

Ref Expression
wel wff x y

Proof of Theorem wel
StepHypRef Expression
1 wcel 1390 1 wff x y
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  9265  bdcint  9266  bdcriota  9272  bdsep2  9274  bdsepnft  9275  bdsepnf  9276  bdsepnfALT  9277  bdzfauscl  9278  bdbm1.3ii  9279  bj-nalset  9280  bdinex1  9284  bj-zfpair2  9295  bj-axun2  9300  bj-uniex2  9301  bj-d0clsepcl  9314  bj-nn0suc0  9338  bj-nntrans  9339  bj-omex2  9361  strcoll2  9367  strcollnft  9368  strcollnf  9369  strcollnfALT  9370  sscoll2  9372
  Copyright terms: Public domain W3C validator