Theorem wel 1711

Description: Extend wff definition to include atomic formulas with the epsilon (membership) predicate. This is read "x is an element of y," "x is a member of y," "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. (epsilon) 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 1711 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 1710. This lets us avoid overloading the e. connective, thus preventing ambiguity that would complicate certain Metamath parsers. However, logically wel 1711 is considered to be a primitive syntax, even though here it is artificially "derived" from wcel 1710. Note: To see the proof steps of this syntax proof, type "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 1710	1 wff x e. y

Syntax hints:   e. wcel 1710

This theorem is referenced by:  elequ1  1713  elequ2  1715  ax11wdemo  1723  cleljust  2014  cleljustALT  2015  dveel1  2019  dveel2  2020  ax15  2021  elsb1  2103  elsb2  2104  ax17el  2189  dveel2ALT  2191  ax11el  2194  unipr  3906  iinuni  4050  axprimlem1  4089  axprimlem2  4090  axxpprim  4091  axcnvprim  4092  axssetprim  4093  axsiprim  4094  axtyplowerprim  4095  axins2prim  4096  axins3prim  4097  ninexg  4098  snex  4112  pwadjoin  4120  1cex  4143  xpkvexg  4286  p6exg  4291  ssetkex  4295  dfuni3  4316  dfint3  4319  unipw1  4326  dfpw2  4328  eqpw1uni  4331  dfaddc2  4382  dfnnc2  4396  peano2  4404  elsuc  4414  nnsucelrlem1  4425  nnsucelr  4429  nndisjeq  4430  prepeano4  4452  ltfinex  4465  ssfin  4471  ncfinraiselem2  4481  ncfinraise  4482  ncfinlowerlem1  4483  ncfinlower  4484  eqtfinrelk  4487  tfin11  4494  tfinsuc  4499  evenfinex  4504  oddfinex  4505  evenodddisjlem1  4516  nnadjoinlem1  4520  nnadjoin  4521  nnpweqlem1  4523  nnpweq  4524  srelk  4525  sfin112  4530  sfindbl  4531  tfinnnlem1  4534  tfinnn  4535  sfinltfin  4536  spfinex  4538  ncvspfin  4539  spfinsfincl  4540  spfininduct  4541  vfinspsslem1  4551  nulnnn  4557  dfop2lem1  4574  setconslem2  4733  dfswap2  4742  epelc  4766  tz6.12-2  5347  chfnrn  5400  funiunfv  5468  releqel  5808  releqmpt2  5810  cupex  5817  composeex  5821  disjex  5824  addcfnex  5825  epprc  5828  crossex  5851  pw1fnex  5853  domfnex  5871  ranfnex  5872  clos1conn  5880  dfnnc3  5886  transex  5911  refex  5912  antisymex  5913  connexex  5914  foundex  5915  extex  5916  symex  5917  qsexg  5983  enpw1  6063  enprmaplem1  6077  enprmaplem4  6080  enprmaplem5  6081  enprmaplem6  6082  nenpw1pwlem1  6085  lecex  6116  mucex  6134  peano4nc  6151  ncssfin  6152  nntccl  6171  ovcelem1  6172  ceexlem1  6174  nc0le1  6217  tcfnex  6245  nmembers1lem1  6269  nchoicelem10  6299  nchoicelem11  6300  nchoicelem16  6305