Theorem wel 1464

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

Proof of Theorem wel

Step	Hyp	Ref	Expression
1		wcel 1463	1 wff x e. y

Syntax hints:   e. wcel 1463

This theorem is referenced by:  elequ1  1673  elequ2  1674  cleljust  1888  elsb3  1927  elsb4  1928  dveel1  1971  dveel2  1972  axext3  2098  axext4  2099  bm1.1  2100  ru  2877  nfuni  3708  nfunid  3709  unieq  3711  inteq  3740  nfint  3747  uniiun  3832  intiin  3833  trint  4001  axsep2  4007  bm1.3ii  4009  zfnuleu  4012  0ex  4015  nalset  4018  vnex  4019  repizf2  4046  axpweq  4055  zfpow  4059  axpow2  4060  axpow3  4061  el  4062  vpwex  4063  dtruarb  4075  exmidn0m  4084  exmidsssn  4085  fr0  4233  wetrep  4242  zfun  4316  axun2  4317  uniuni  4332  regexmid  4410  zfregfr  4448  ordwe  4450  wessep  4452  nnregexmid  4494  rele  4629  funimaexglem  5164  acexmidlem2  5725  acexmid  5727  dfsmo2  6138  smores2  6145  tfrcllemsucaccv  6205  findcard2d  6738  exmidfodomr  7008  acfun  7011  ccfunen  7027  ltsopi  7076  fnn0nninf  10103  fsum2dlemstep  11095  exmidunben  11784  isbasis3g  12056  tgcl  12076  tgss2  12091  blbas  12422  metrest  12495  bdcuni  12766  bdcint  12767  bdcriota  12773  bdsep1  12775  bdsep2  12776  bdsepnft  12777  bdsepnf  12778  bdsepnfALT  12779  bdzfauscl  12780  bdbm1.3ii  12781  bj-axemptylem  12782  bj-axempty  12783  bj-axempty2  12784  bj-nalset  12785  bdinex1  12789  bj-zfpair2  12800  bj-axun2  12805  bj-uniex2  12806  bj-d0clsepcl  12815  bj-nn0suc0  12840  bj-nntrans  12841  bj-omex2  12867  strcoll2  12873  strcollnft  12874  strcollnf  12875  strcollnfALT  12876  sscoll2  12878  nninfsellemcl  12899  nninfsellemsuc  12900  nninfsellemqall  12903  nninfomni  12907  exmidsbthrlem  12909