Theorem wel 1481

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

Syntax hints:   e. wcel 1480

This theorem is referenced by:  elequ1  1690  elequ2  1691  cleljust  1908  elsb3  1949  elsb4  1950  dveel1  1993  dveel2  1994  axext3  2120  axext4  2121  bm1.1  2122  ru  2903  nfuni  3737  nfunid  3738  unieq  3740  inteq  3769  nfint  3776  uniiun  3861  intiin  3862  trint  4036  axsep2  4042  bm1.3ii  4044  zfnuleu  4047  0ex  4050  nalset  4053  vnex  4054  repizf2  4081  axpweq  4090  zfpow  4094  axpow2  4095  axpow3  4096  el  4097  vpwex  4098  dtruarb  4110  exmidn0m  4119  exmidsssn  4120  fr0  4268  wetrep  4277  zfun  4351  axun2  4352  uniuni  4367  regexmid  4445  zfregfr  4483  ordwe  4485  wessep  4487  nnregexmid  4529  rele  4664  funimaexglem  5201  acexmidlem2  5764  acexmid  5766  dfsmo2  6177  smores2  6184  tfrcllemsucaccv  6244  findcard2d  6778  exmidfodomr  7053  acfun  7056  ccfunen  7072  ltsopi  7121  fnn0nninf  10203  fsum2dlemstep  11196  exmidunben  11928  isbasis3g  12202  tgcl  12222  tgss2  12237  blbas  12591  metrest  12664  bdcuni  13063  bdcint  13064  bdcriota  13070  bdsep1  13072  bdsep2  13073  bdsepnft  13074  bdsepnf  13075  bdsepnfALT  13076  bdzfauscl  13077  bdbm1.3ii  13078  bj-axemptylem  13079  bj-axempty  13080  bj-axempty2  13081  bj-nalset  13082  bdinex1  13086  bj-zfpair2  13097  bj-axun2  13102  bj-uniex2  13103  bj-d0clsepcl  13112  bj-nn0suc0  13137  bj-nntrans  13138  bj-omex2  13164  strcoll2  13170  strcollnft  13171  strcollnf  13172  strcollnfALT  13173  sscoll2  13175  nninfsellemcl  13196  nninfsellemsuc  13197  nninfsellemqall  13200  nninfomni  13204  exmidsbthrlem  13206