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  1910  elsb3  1951  elsb4  1952  dveel1  1995  dveel2  1996  axext3  2122  axext4  2123  bm1.1  2124  ru  2908  nfuni  3742  nfunid  3743  unieq  3745  inteq  3774  nfint  3781  uniiun  3866  intiin  3867  trint  4041  axsep2  4047  bm1.3ii  4049  zfnuleu  4052  0ex  4055  nalset  4058  vnex  4059  repizf2  4086  axpweq  4095  zfpow  4099  axpow2  4100  axpow3  4101  el  4102  vpwex  4103  dtruarb  4115  exmidn0m  4124  exmidsssn  4125  fr0  4273  wetrep  4282  zfun  4356  axun2  4357  uniuni  4372  regexmid  4450  zfregfr  4488  ordwe  4490  wessep  4492  nnregexmid  4534  rele  4669  funimaexglem  5206  acexmidlem2  5771  acexmid  5773  dfsmo2  6184  smores2  6191  tfrcllemsucaccv  6251  findcard2d  6785  exmidfodomr  7060  acfun  7063  ccfunen  7079  ltsopi  7128  fnn0nninf  10210  fsum2dlemstep  11203  exmidunben  11939  isbasis3g  12213  tgcl  12233  tgss2  12248  blbas  12602  metrest  12675  bdcuni  13074  bdcint  13075  bdcriota  13081  bdsep1  13083  bdsep2  13084  bdsepnft  13085  bdsepnf  13086  bdsepnfALT  13087  bdzfauscl  13088  bdbm1.3ii  13089  bj-axemptylem  13090  bj-axempty  13091  bj-axempty2  13092  bj-nalset  13093  bdinex1  13097  bj-zfpair2  13108  bj-axun2  13113  bj-uniex2  13114  bj-d0clsepcl  13123  bj-nn0suc0  13148  bj-nntrans  13149  bj-omex2  13175  strcoll2  13181  strcollnft  13182  strcollnf  13183  strcollnfALT  13184  sscoll2  13186  nninfsellemcl  13207  nninfsellemsuc  13208  nninfsellemqall  13211  nninfomni  13215  exmidsbthrlem  13217