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

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

Proof of Theorem wel
StepHypRef Expression
1 wcel 1436 1  wff  x  e.  y
Colors of variables: wff set class
Syntax hints:    e. wcel 1436
This theorem is referenced by:  elequ1  1644  elequ2  1645  cleljust  1858  elsb3  1897  elsb4  1898  dveel1  1941  dveel2  1942  axext3  2068  axext4  2069  bm1.1  2070  ru  2828  nfuni  3642  nfunid  3643  unieq  3645  inteq  3674  nfint  3681  uniiun  3766  intiin  3767  trint  3926  axsep2  3933  bm1.3ii  3935  zfnuleu  3938  0ex  3941  nalset  3944  vnex  3945  repizf2  3972  axpweq  3981  zfpow  3985  axpow2  3986  axpow3  3987  el  3988  vpwex  3989  dtruarb  4000  fr0  4152  wetrep  4161  zfun  4235  axun2  4236  uniuni  4247  regexmid  4324  zfregfr  4362  ordwe  4364  wessep  4366  nnregexmid  4407  rele  4534  funimaexglem  5062  acexmidlem2  5610  acexmid  5612  dfsmo2  6006  smores2  6013  tfrcllemsucaccv  6073  findcard2d  6559  exmidfodomr  6774  ltsopi  6823  fnn0nninf  9771  bdcuni  11212  bdcint  11213  bdcriota  11219  bdsep1  11221  bdsep2  11222  bdsepnft  11223  bdsepnf  11224  bdsepnfALT  11225  bdzfauscl  11226  bdbm1.3ii  11227  bj-axemptylem  11228  bj-axempty  11229  bj-axempty2  11230  bj-nalset  11231  bdinex1  11235  bj-zfpair2  11246  bj-axun2  11251  bj-uniex2  11252  bj-d0clsepcl  11265  bj-nn0suc0  11290  bj-nntrans  11291  bj-omex2  11317  strcoll2  11323  strcollnft  11324  strcollnf  11325  strcollnfALT  11326  sscoll2  11328  nninfsellemcl  11348  nninfsellemsuc  11349  nninfsellemqall  11352  nninfomni  11356  exmidsbthrlem  11357
  Copyright terms: Public domain W3C validator