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  6562  smores2  6569  tfrcllemsucaccv  6629  pw2f1odclem  7138  findcard2d  7199  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  10896  hashfibclem  11304  fsum2dlemstep  12226  fprod2dlemstep  12414  exmidunben  13375  gsumresfi  14263  gsum2dfilem2  14272  prdsex  14279  isbasis3g  15272  tgcl  15290  tgss2  15305  blbas  15659  metrest  15732  dvmptfsum  15951  uhgrfm  16519  ushgrfm  16520  uhgrss  16521  uhgreq12g  16522  uhgrfun  16523  ushgruhgr  16526  isuhgropm  16527  uhgr0e  16528  uhgr0vb  16530  uhgr0  16531  uhgrun  16532  bdcuni  17107  bdcint  17108  bdcriota  17114  bdsep1  17116  bdsep2  17117  bdsepnft  17118  bdsepnf  17119  bdsepnfALT  17120  bdsepg  17121  bdbm1.3ii  17122  bj-axemptylem  17123  bj-axempty  17124  bj-axempty2  17125  bj-nalset  17126  bdinex1  17130  bj-zfpair2  17141  bj-axun2  17146  bj-uniex2  17147  bj-d0clsepcl  17156  bj-nn0suc0  17181  bj-nntrans  17182  bj-omex2  17208  strcollnft  17215  sscoll2  17219  nninfsellemcl  17260  nninfsellemsuc  17261  nninfsellemqall  17264  nninfomni  17268  exmidsbthrlem  17273