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

Syntax hints:   e. wcel 2209

This theorem is referenced 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  3939  nfunid  3940  unieq  3942  inteq  3971  nfint  3978  uniiun  4064  intiin  4065  trint  4242  axsepg  4248  sepg  4249  sepgi  4250  bm1.3ii  4252  zfnuleu  4255  0ex  4258  nalset  4261  vnex  4262  repizf2  4297  axpweq  4306  zfpow  4310  axpow2  4311  axpow3  4312  el  4313  vpwex  4314  dtruarb  4326  exmidn0m  4336  exmidsssn  4337  fr0  4494  wetrep  4503  zfun  4577  axun2  4578  uniex2  4579  uniuni  4595  regexmid  4680  zfregfr  4719  ordwe  4721  wessep  4723  nnregexmid  4766  rele  4908  funimaexglem  5462  acexmidlem2  6075  acexmid  6077  dfsmo2  6551  smores2  6558  tfrcllemsucaccv  6618  pw2f1odclem  7127  findcard2d  7188  sspw1or2  7537  exmidfodomr  7549  acfun  7556  exmidontriimlem3  7572  exmidontriimlem4  7573  exmidontriim  7574  onntri13  7590  exmidontri  7591  onntri51  7592  onntri3or  7597  exmidmotap  7620  ccfunen  7623  cc1  7624  ltsopi  7680  fnn0nninf  10856  hashfibclem  11263  fsum2dlemstep  12182  fprod2dlemstep  12370  exmidunben  13298  prdsex  14152  isbasis3g  15073  tgcl  15091  tgss2  15106  blbas  15460  metrest  15533  dvmptfsum  15752  uhgrfm  16231  ushgrfm  16232  uhgrss  16233  uhgreq12g  16234  uhgrfun  16235  ushgruhgr  16238  isuhgropm  16239  uhgr0e  16240  uhgr0vb  16242  uhgr0  16243  uhgrun  16244  bdcuni  16819  bdcint  16820  bdcriota  16826  bdsep1  16828  bdsep2  16829  bdsepnft  16830  bdsepnf  16831  bdsepnfALT  16832  bdsepg  16833  bdbm1.3ii  16834  bj-axemptylem  16835  bj-axempty  16836  bj-axempty2  16837  bj-nalset  16838  bdinex1  16842  bj-zfpair2  16853  bj-axun2  16858  bj-uniex2  16859  bj-d0clsepcl  16868  bj-nn0suc0  16893  bj-nntrans  16894  bj-omex2  16920  strcollnft  16927  sscoll2  16931  nninfsellemcl  16962  nninfsellemsuc  16963  nninfsellemqall  16966  nninfomni  16970  exmidsbthrlem  16975