Theorem wel 2177

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

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

Syntax hints:   e. wcel 2176

This theorem is referenced by:  elequ1  2180  elequ2  2181  cleljust  2182  elsb1  2183  elsb2  2184  dveel1  2185  dveel2  2186  axext3  2188  axext4  2189  bm1.1  2190  ru  2997  nfuni  3856  nfunid  3857  unieq  3859  inteq  3888  nfint  3895  uniiun  3981  intiin  3982  trint  4158  axsep2  4164  bm1.3ii  4166  zfnuleu  4169  0ex  4172  nalset  4175  vnex  4176  repizf2  4207  axpweq  4216  zfpow  4220  axpow2  4221  axpow3  4222  el  4223  vpwex  4224  dtruarb  4236  exmidn0m  4246  exmidsssn  4247  fr0  4399  wetrep  4408  zfun  4482  axun2  4483  uniuni  4499  regexmid  4584  zfregfr  4623  ordwe  4625  wessep  4627  nnregexmid  4670  rele  4809  funimaexglem  5358  acexmidlem2  5943  acexmid  5945  dfsmo2  6375  smores2  6382  tfrcllemsucaccv  6442  pw2f1odclem  6933  findcard2d  6990  exmidfodomr  7314  acfun  7321  exmidontriimlem3  7337  exmidontriimlem4  7338  exmidontriim  7339  onntri13  7352  exmidontri  7353  onntri51  7354  onntri3or  7359  exmidmotap  7375  ccfunen  7378  cc1  7379  ltsopi  7435  fnn0nninf  10585  fsum2dlemstep  11778  fprod2dlemstep  11966  exmidunben  12830  prdsex  13134  isbasis3g  14551  tgcl  14569  tgss2  14584  blbas  14938  metrest  15011  dvmptfsum  15230  bdcuni  15849  bdcint  15850  bdcriota  15856  bdsep1  15858  bdsep2  15859  bdsepnft  15860  bdsepnf  15861  bdsepnfALT  15862  bdzfauscl  15863  bdbm1.3ii  15864  bj-axemptylem  15865  bj-axempty  15866  bj-axempty2  15867  bj-nalset  15868  bdinex1  15872  bj-zfpair2  15883  bj-axun2  15888  bj-uniex2  15889  bj-d0clsepcl  15898  bj-nn0suc0  15923  bj-nntrans  15924  bj-omex2  15950  strcollnft  15957  sscoll2  15961  nninfsellemcl  15985  nninfsellemsuc  15986  nninfsellemqall  15989  nninfomni  15993  exmidsbthrlem  15998