Theorem wel 2210

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

This proof depends on syntax axioms:   e. wcel 2209

This theorem is used by:  elequ1  2213  elequ2  2214  cleljust  2215  elsb1  2216  elsb2  2217  dveel1  2218  dveel2  2219  axext3  2221  axext4  2222  bm1.1  2223  ru  3050  nfuni  3941  nfunid  3942  unieq  3944  inteq  3973  nfint  3980  uniiun  4066  intiin  4067  trint  4246  axsepg  4252  sepg  4253  sepgi  4254  bm1.3ii  4256  zfnuleu  4259  0ex  4262  nalset  4265  vnex  4266  repizf2  4301  axpweq  4310  zfpow  4314  axpow2  4315  axpow3  4316  el  4317  vpwex  4318  dtruarb  4330  exmidn0m  4340  exmidsssn  4341  fr0  4498  wetrep  4507  zfun  4581  axun2  4582  uniex2  4583  uniuni  4599  regexmid  4684  zfregfr  4723  ordwe  4725  wessep  4727  nnregexmid  4770  rele  4912  funimaexglem  5467  acexmidlem2  6085  acexmid  6087  dfsmo2  6563  smores2  6570  tfrcllemsucaccv  6630  pw2f1odclem  7140  findcard2d  7201  sspw1or2  7550  exmidfodomr  7562  acfun  7569  exmidontriimlem3  7585  exmidontriimlem4  7586  exmidontriim  7587  onntri13  7603  exmidontri  7604  onntri51  7605  onntri3or  7610  exmidmotap  7633  ccfunen  7636  cc1  7637  ltsopi  7693  fnn0nninf  10895  hashfibclem  11303  fsum2dlemstep  12225  fprod2dlemstep  12413  exmidunben  13374  gsumresfi  14262  gsum2dfilem2  14271  prdsex  14278  isbasis3g  15289  tgcl  15307  tgss2  15322  blbas  15676  metrest  15749  dvmptfsum  15968  uhgrfm  16536  ushgrfm  16537  uhgrss  16538  uhgreq12g  16539  uhgrfun  16540  ushgruhgr  16543  isuhgropm  16544  uhgr0e  16545  uhgr0vb  16547  uhgr0  16548  uhgrun  16549  bdcuni  17124  bdcint  17125  bdcriota  17131  bdsep1  17133  bdsep2  17134  bdsepnft  17135  bdsepnf  17136  bdsepnfALT  17137  bdsepg  17138  bdbm1.3ii  17139  bj-axemptylem  17140  bj-axempty  17141  bj-axempty2  17142  bj-nalset  17143  bdinex1  17147  bj-zfpair2  17158  bj-axun2  17163  bj-uniex2  17164  bj-d0clsepcl  17173  bj-nn0suc0  17198  bj-nntrans  17199  bj-omex2  17225  strcollnft  17232  sscoll2  17236  nninfsellemcl  17277  nninfsellemsuc  17278  nninfsellemqall  17281  nninfomni  17285  exmidsbthrlem  17290