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

Theorem wel 1394
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 1394 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 1393. This lets us avoid overloading the connective, thus preventing ambiguity that would complicate certain Metamath parsers. However, logically wel 1394 is considered to be a primitive syntax, even though here it is artificially "derived" from wcel 1393. 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 𝑥𝑦

Proof of Theorem wel
StepHypRef Expression
1 wcel 1393 1 wff 𝑥𝑦
Colors of variables: wff set class
Syntax hints:  wcel 1393
This theorem is referenced by:  elequ1  1600  elequ2  1601  cleljust  1813  elsb3  1852  elsb4  1853  dveel1  1896  dveel2  1897  axext3  2023  axext4  2024  bm1.1  2025  ru  2763  nfuni  3586  nfunid  3587  unieq  3589  inteq  3618  nfint  3625  uniiun  3710  intiin  3711  trint  3869  axsep2  3876  bm1.3ii  3878  zfnuleu  3881  0ex  3884  nalset  3887  repizf2  3915  axpweq  3924  zfpow  3928  axpow2  3929  axpow3  3930  el  3931  dtruarb  3942  fr0  4088  wetrep  4097  zfun  4171  axun2  4172  uniuni  4183  regexmid  4260  zfregfr  4298  ordwe  4300  wessep  4302  nnregexmid  4342  rele  4466  funimaexglem  4982  acexmidlem2  5509  acexmid  5511  dfsmo2  5902  smores2  5909  findcard2d  6348  ltsopi  6418  bdcuni  9996  bdcint  9997  bdcriota  10003  bdsep1  10005  bdsep2  10006  bdsepnft  10007  bdsepnf  10008  bdsepnfALT  10009  bdzfauscl  10010  bdbm1.3ii  10011  bj-axemptylem  10012  bj-axempty  10013  bj-axempty2  10014  bj-nalset  10015  bdinex1  10019  bj-zfpair2  10030  bj-axun2  10035  bj-uniex2  10036  bj-d0clsepcl  10049  bj-nn0suc0  10075  bj-nntrans  10076  bj-omex2  10102  strcoll2  10108  strcollnft  10109  strcollnf  10110  strcollnfALT  10111  sscoll2  10113
  Copyright terms: Public domain W3C validator