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

Theorem wel 2149
Description: Extend wff definition to include atomic formulas with the membership predicate. This is read either " x is an element of 
y", or " x is a member of  y", or " 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. 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 2149 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 2148. This lets us avoid overloading the  e. connective, thus preventing ambiguity that would complicate certain Metamath parsers. However, logically wel 2149 is considered to be a primitive syntax, even though here it is artificially "derived" from wcel 2148. Note: To see the proof steps of this syntax proof, type "MM> 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 2148 1  wff  x  e.  y
Colors of variables: wff set class
Syntax hints:    e. wcel 2148
This theorem is referenced by:  elequ1  2152  elequ2  2153  cleljust  2154  elsb1  2155  elsb2  2156  dveel1  2157  dveel2  2158  axext3  2160  axext4  2161  bm1.1  2162  ru  2961  nfuni  3815  nfunid  3816  unieq  3818  inteq  3847  nfint  3854  uniiun  3939  intiin  3940  trint  4115  axsep2  4121  bm1.3ii  4123  zfnuleu  4126  0ex  4129  nalset  4132  vnex  4133  repizf2  4161  axpweq  4170  zfpow  4174  axpow2  4175  axpow3  4176  el  4177  vpwex  4178  dtruarb  4190  exmidn0m  4200  exmidsssn  4201  fr0  4350  wetrep  4359  zfun  4433  axun2  4434  uniuni  4450  regexmid  4533  zfregfr  4572  ordwe  4574  wessep  4576  nnregexmid  4619  rele  4756  funimaexglem  5298  acexmidlem2  5869  acexmid  5871  dfsmo2  6285  smores2  6292  tfrcllemsucaccv  6352  findcard2d  6888  exmidfodomr  7200  acfun  7203  exmidontriimlem3  7219  exmidontriimlem4  7220  exmidontriim  7221  onntri13  7234  exmidontri  7235  onntri51  7236  onntri3or  7241  exmidmotap  7257  ccfunen  7260  cc1  7261  ltsopi  7316  fnn0nninf  10432  fsum2dlemstep  11435  fprod2dlemstep  11623  exmidunben  12419  isbasis3g  13415  tgcl  13435  tgss2  13450  blbas  13804  metrest  13877  bdcuni  14488  bdcint  14489  bdcriota  14495  bdsep1  14497  bdsep2  14498  bdsepnft  14499  bdsepnf  14500  bdsepnfALT  14501  bdzfauscl  14502  bdbm1.3ii  14503  bj-axemptylem  14504  bj-axempty  14505  bj-axempty2  14506  bj-nalset  14507  bdinex1  14511  bj-zfpair2  14522  bj-axun2  14527  bj-uniex2  14528  bj-d0clsepcl  14537  bj-nn0suc0  14562  bj-nntrans  14563  bj-omex2  14589  strcollnft  14596  sscoll2  14600  nninfsellemcl  14620  nninfsellemsuc  14621  nninfsellemqall  14624  nninfomni  14628  exmidsbthrlem  14630
  Copyright terms: Public domain W3C validator