ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  wel 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  9331  bdcint  9332  bdcriota  9338  bdsep1  9340  bdsep2  9341  bdsepnft  9342  bdsepnf  9343  bdsepnfALT  9344  bdzfauscl  9345  bdbm1.3ii  9346  bj-axemptylem  9347  bj-axempty  9348  bj-axempty2  9349  bj-nalset  9350  bdinex1  9354  bj-zfpair2  9365  bj-axun2  9370  bj-uniex2  9371  bj-d0clsepcl  9384  bj-nn0suc0  9410  bj-nntrans  9411  bj-omex2  9437  strcoll2  9443  strcollnft  9444  strcollnf  9445  strcollnfALT  9446  sscoll2  9448
  Copyright terms: Public domain W3C validator