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

Theorem wel 1437
Description: Extend wff definition to include atomic formulas with the epsilon (membership) predicate. This is read "𝑥 is an element of 𝑦," "𝑥 is a member of 𝑦," "𝑥 belongs to 𝑦," or "𝑦 contains 𝑥." Note: The phrase "𝑦 includes 𝑥 " means "𝑥 is a subset of 𝑦;" to use it also for 𝑥𝑦, 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 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 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 𝑥𝑦

Proof of Theorem wel
StepHypRef Expression
1 wcel 1436 1 wff 𝑥𝑦
Colors of variables: wff set class
Syntax hints:  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  3925  axsep2  3932  bm1.3ii  3934  zfnuleu  3937  0ex  3940  nalset  3943  vnex  3944  repizf2  3971  axpweq  3980  zfpow  3984  axpow2  3985  axpow3  3986  el  3987  vpwex  3988  dtruarb  3999  fr0  4151  wetrep  4160  zfun  4234  axun2  4235  uniuni  4246  regexmid  4323  zfregfr  4361  ordwe  4363  wessep  4365  nnregexmid  4406  rele  4533  funimaexglem  5059  acexmidlem2  5604  acexmid  5606  dfsmo2  6000  smores2  6007  tfrcllemsucaccv  6067  findcard2d  6553  exmidfodomr  6767  ltsopi  6816  fnn0nninf  9764  bdcuni  11197  bdcint  11198  bdcriota  11204  bdsep1  11206  bdsep2  11207  bdsepnft  11208  bdsepnf  11209  bdsepnfALT  11210  bdzfauscl  11211  bdbm1.3ii  11212  bj-axemptylem  11213  bj-axempty  11214  bj-axempty2  11215  bj-nalset  11216  bdinex1  11220  bj-zfpair2  11231  bj-axun2  11236  bj-uniex2  11237  bj-d0clsepcl  11250  bj-nn0suc0  11275  bj-nntrans  11276  bj-omex2  11302  strcoll2  11308  strcollnft  11309  strcollnf  11310  strcollnfALT  11311  sscoll2  11313  nninfsellemcl  11333  nninfsellemsuc  11334  nninfsellemqall  11337  nninfomni  11341  exmidsbthrlem  11342
  Copyright terms: Public domain W3C validator