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

Theorem wel 1410
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 1410 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 1409. This lets us avoid overloading the  e. connective, thus preventing ambiguity that would complicate certain Metamath parsers. However, logically wel 1410 is considered to be a primitive syntax, even though here it is artificially "derived" from wcel 1409. 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 1409 1  wff  x  e.  y
Colors of variables: wff set class
Syntax hints:    e. wcel 1409
This theorem is referenced by:  elequ1  1616  elequ2  1617  cleljust  1829  elsb3  1868  elsb4  1869  dveel1  1912  dveel2  1913  axext3  2039  axext4  2040  bm1.1  2041  ru  2786  nfuni  3614  nfunid  3615  unieq  3617  inteq  3646  nfint  3653  uniiun  3738  intiin  3739  trint  3897  axsep2  3904  bm1.3ii  3906  zfnuleu  3909  0ex  3912  nalset  3915  repizf2  3943  axpweq  3952  zfpow  3956  axpow2  3957  axpow3  3958  el  3959  dtruarb  3970  fr0  4116  wetrep  4125  zfun  4199  axun2  4200  uniuni  4211  regexmid  4288  zfregfr  4326  ordwe  4328  wessep  4330  nnregexmid  4370  rele  4494  funimaexglem  5010  acexmidlem2  5537  acexmid  5539  dfsmo2  5933  smores2  5940  findcard2d  6379  ltsopi  6476  bdcuni  10383  bdcint  10384  bdcriota  10390  bdsep1  10392  bdsep2  10393  bdsepnft  10394  bdsepnf  10395  bdsepnfALT  10396  bdzfauscl  10397  bdbm1.3ii  10398  bj-axemptylem  10399  bj-axempty  10400  bj-axempty2  10401  bj-nalset  10402  bdinex1  10406  bj-zfpair2  10417  bj-axun2  10422  bj-uniex2  10423  bj-d0clsepcl  10436  bj-nn0suc0  10462  bj-nntrans  10463  bj-omex2  10489  strcoll2  10495  strcollnft  10496  strcollnf  10497  strcollnfALT  10498  sscoll2  10500
  Copyright terms: Public domain W3C validator