Theorem wel 2165

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

Syntax hints:   e. wcel 2164

This theorem is referenced by:  elequ1  2168  elequ2  2169  cleljust  2170  elsb1  2171  elsb2  2172  dveel1  2173  dveel2  2174  axext3  2176  axext4  2177  bm1.1  2178  ru  2985  nfuni  3842  nfunid  3843  unieq  3845  inteq  3874  nfint  3881  uniiun  3967  intiin  3968  trint  4143  axsep2  4149  bm1.3ii  4151  zfnuleu  4154  0ex  4157  nalset  4160  vnex  4161  repizf2  4192  axpweq  4201  zfpow  4205  axpow2  4206  axpow3  4207  el  4208  vpwex  4209  dtruarb  4221  exmidn0m  4231  exmidsssn  4232  fr0  4383  wetrep  4392  zfun  4466  axun2  4467  uniuni  4483  regexmid  4568  zfregfr  4607  ordwe  4609  wessep  4611  nnregexmid  4654  rele  4793  funimaexglem  5338  acexmidlem2  5916  acexmid  5918  dfsmo2  6342  smores2  6349  tfrcllemsucaccv  6409  pw2f1odclem  6892  findcard2d  6949  exmidfodomr  7266  acfun  7269  exmidontriimlem3  7285  exmidontriimlem4  7286  exmidontriim  7287  onntri13  7300  exmidontri  7301  onntri51  7302  onntri3or  7307  exmidmotap  7323  ccfunen  7326  cc1  7327  ltsopi  7382  fnn0nninf  10512  fsum2dlemstep  11580  fprod2dlemstep  11768  exmidunben  12586  prdsex  12883  isbasis3g  14225  tgcl  14243  tgss2  14258  blbas  14612  metrest  14685  dvmptfsum  14904  bdcuni  15438  bdcint  15439  bdcriota  15445  bdsep1  15447  bdsep2  15448  bdsepnft  15449  bdsepnf  15450  bdsepnfALT  15451  bdzfauscl  15452  bdbm1.3ii  15453  bj-axemptylem  15454  bj-axempty  15455  bj-axempty2  15456  bj-nalset  15457  bdinex1  15461  bj-zfpair2  15472  bj-axun2  15477  bj-uniex2  15478  bj-d0clsepcl  15487  bj-nn0suc0  15512  bj-nntrans  15513  bj-omex2  15539  strcollnft  15546  sscoll2  15550  nninfsellemcl  15571  nninfsellemsuc  15572  nninfsellemqall  15575  nninfomni  15579  exmidsbthrlem  15582