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

Theorem wel 1466
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 1466 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 1465. This lets us avoid overloading the connective, thus preventing ambiguity that would complicate certain Metamath parsers. However, logically wel 1466 is considered to be a primitive syntax, even though here it is artificially "derived" from wcel 1465. 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 1465 1 wff 𝑥𝑦
Colors of variables: wff set class
Syntax hints:  wcel 1465
This theorem is referenced by:  elequ1  1675  elequ2  1676  cleljust  1890  elsb3  1929  elsb4  1930  dveel1  1973  dveel2  1974  axext3  2100  axext4  2101  bm1.1  2102  ru  2881  nfuni  3712  nfunid  3713  unieq  3715  inteq  3744  nfint  3751  uniiun  3836  intiin  3837  trint  4011  axsep2  4017  bm1.3ii  4019  zfnuleu  4022  0ex  4025  nalset  4028  vnex  4029  repizf2  4056  axpweq  4065  zfpow  4069  axpow2  4070  axpow3  4071  el  4072  vpwex  4073  dtruarb  4085  exmidn0m  4094  exmidsssn  4095  fr0  4243  wetrep  4252  zfun  4326  axun2  4327  uniuni  4342  regexmid  4420  zfregfr  4458  ordwe  4460  wessep  4462  nnregexmid  4504  rele  4639  funimaexglem  5176  acexmidlem2  5739  acexmid  5741  dfsmo2  6152  smores2  6159  tfrcllemsucaccv  6219  findcard2d  6753  exmidfodomr  7028  acfun  7031  ccfunen  7047  ltsopi  7096  fnn0nninf  10178  fsum2dlemstep  11171  exmidunben  11866  isbasis3g  12140  tgcl  12160  tgss2  12175  blbas  12529  metrest  12602  bdcuni  13001  bdcint  13002  bdcriota  13008  bdsep1  13010  bdsep2  13011  bdsepnft  13012  bdsepnf  13013  bdsepnfALT  13014  bdzfauscl  13015  bdbm1.3ii  13016  bj-axemptylem  13017  bj-axempty  13018  bj-axempty2  13019  bj-nalset  13020  bdinex1  13024  bj-zfpair2  13035  bj-axun2  13040  bj-uniex2  13041  bj-d0clsepcl  13050  bj-nn0suc0  13075  bj-nntrans  13076  bj-omex2  13102  strcoll2  13108  strcollnft  13109  strcollnf  13110  strcollnfALT  13111  sscoll2  13113  nninfsellemcl  13134  nninfsellemsuc  13135  nninfsellemqall  13138  nninfomni  13142  exmidsbthrlem  13144
  Copyright terms: Public domain W3C validator