Theorem wel 2203

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

Syntax hints:   e. wcel 2202

This theorem is referenced by:  elequ1  2206  elequ2  2207  cleljust  2208  elsb1  2209  elsb2  2210  dveel1  2211  dveel2  2212  axext3  2214  axext4  2215  bm1.1  2216  ru  3030  nfuni  3899  nfunid  3900  unieq  3902  inteq  3931  nfint  3938  uniiun  4024  intiin  4025  trint  4202  axsep2  4208  bm1.3ii  4210  zfnuleu  4213  0ex  4216  nalset  4219  vnex  4220  repizf2  4252  axpweq  4261  zfpow  4265  axpow2  4266  axpow3  4267  el  4268  vpwex  4269  dtruarb  4281  exmidn0m  4291  exmidsssn  4292  fr0  4448  wetrep  4457  zfun  4531  axun2  4532  uniuni  4548  regexmid  4633  zfregfr  4672  ordwe  4674  wessep  4676  nnregexmid  4719  rele  4860  funimaexglem  5413  acexmidlem2  6015  acexmid  6017  dfsmo2  6453  smores2  6460  tfrcllemsucaccv  6520  pw2f1odclem  7020  findcard2d  7080  sspw1or2  7403  exmidfodomr  7415  acfun  7422  exmidontriimlem3  7438  exmidontriimlem4  7439  exmidontriim  7440  onntri13  7456  exmidontri  7457  onntri51  7458  onntri3or  7463  exmidmotap  7480  ccfunen  7483  cc1  7484  ltsopi  7540  fnn0nninf  10700  fsum2dlemstep  11996  fprod2dlemstep  12184  exmidunben  13048  prdsex  13353  isbasis3g  14772  tgcl  14790  tgss2  14805  blbas  15159  metrest  15232  dvmptfsum  15451  uhgrfm  15926  ushgrfm  15927  uhgrss  15928  uhgreq12g  15929  uhgrfun  15930  ushgruhgr  15933  isuhgropm  15934  uhgr0e  15935  uhgr0vb  15937  uhgr0  15938  uhgrun  15939  bdcuni  16474  bdcint  16475  bdcriota  16481  bdsep1  16483  bdsep2  16484  bdsepnft  16485  bdsepnf  16486  bdsepnfALT  16487  bdzfauscl  16488  bdbm1.3ii  16489  bj-axemptylem  16490  bj-axempty  16491  bj-axempty2  16492  bj-nalset  16493  bdinex1  16497  bj-zfpair2  16508  bj-axun2  16513  bj-uniex2  16514  bj-d0clsepcl  16523  bj-nn0suc0  16548  bj-nntrans  16549  bj-omex2  16575  strcollnft  16582  sscoll2  16586  nninfsellemcl  16616  nninfsellemsuc  16617  nninfsellemqall  16620  nninfomni  16624  exmidsbthrlem  16629