Theorem wel 2206

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

Syntax hints:   e. wcel 2205

This theorem is referenced by:  elequ1  2209  elequ2  2210  cleljust  2211  elsb1  2212  elsb2  2213  dveel1  2214  dveel2  2215  axext3  2217  axext4  2218  bm1.1  2219  ru  3043  nfuni  3922  nfunid  3923  unieq  3925  inteq  3954  nfint  3961  uniiun  4047  intiin  4048  trint  4225  axsep2  4231  bm1.3ii  4233  zfnuleu  4236  0ex  4239  nalset  4242  vnex  4243  repizf2  4277  axpweq  4286  zfpow  4290  axpow2  4291  axpow3  4292  el  4293  vpwex  4294  dtruarb  4306  exmidn0m  4316  exmidsssn  4317  fr0  4474  wetrep  4483  zfun  4557  axun2  4558  uniuni  4574  regexmid  4659  zfregfr  4698  ordwe  4700  wessep  4702  nnregexmid  4745  rele  4887  funimaexglem  5441  acexmidlem2  6049  acexmid  6051  dfsmo2  6520  smores2  6527  tfrcllemsucaccv  6587  pw2f1odclem  7089  findcard2d  7150  sspw1or2  7497  exmidfodomr  7509  acfun  7516  exmidontriimlem3  7532  exmidontriimlem4  7533  exmidontriim  7534  onntri13  7550  exmidontri  7551  onntri51  7552  onntri3or  7557  exmidmotap  7577  ccfunen  7580  cc1  7581  ltsopi  7637  fnn0nninf  10804  hashfibclem  11210  fsum2dlemstep  12124  fprod2dlemstep  12312  exmidunben  13194  prdsex  13499  isbasis3g  14928  tgcl  14946  tgss2  14961  blbas  15315  metrest  15388  dvmptfsum  15607  uhgrfm  16085  ushgrfm  16086  uhgrss  16087  uhgreq12g  16088  uhgrfun  16089  ushgruhgr  16092  isuhgropm  16093  uhgr0e  16094  uhgr0vb  16096  uhgr0  16097  uhgrun  16098  bdcuni  16663  bdcint  16664  bdcriota  16670  bdsep1  16672  bdsep2  16673  bdsepnft  16674  bdsepnf  16675  bdsepnfALT  16676  bdzfauscl  16677  bdbm1.3ii  16678  bj-axemptylem  16679  bj-axempty  16680  bj-axempty2  16681  bj-nalset  16682  bdinex1  16686  bj-zfpair2  16697  bj-axun2  16702  bj-uniex2  16703  bj-d0clsepcl  16712  bj-nn0suc0  16737  bj-nntrans  16738  bj-omex2  16764  strcollnft  16771  sscoll2  16775  nninfsellemcl  16806  nninfsellemsuc  16807  nninfsellemqall  16810  nninfomni  16814  exmidsbthrlem  16819