Theorem wel 2149

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

Syntax hints:   e. wcel 2148

This theorem is referenced by:  elequ1  2152  elequ2  2153  cleljust  2154  elsb1  2155  elsb2  2156  dveel1  2157  dveel2  2158  axext3  2160  axext4  2161  bm1.1  2162  ru  2962  nfuni  3816  nfunid  3817  unieq  3819  inteq  3848  nfint  3855  uniiun  3941  intiin  3942  trint  4117  axsep2  4123  bm1.3ii  4125  zfnuleu  4128  0ex  4131  nalset  4134  vnex  4135  repizf2  4163  axpweq  4172  zfpow  4176  axpow2  4177  axpow3  4178  el  4179  vpwex  4180  dtruarb  4192  exmidn0m  4202  exmidsssn  4203  fr0  4352  wetrep  4361  zfun  4435  axun2  4436  uniuni  4452  regexmid  4535  zfregfr  4574  ordwe  4576  wessep  4578  nnregexmid  4621  rele  4758  funimaexglem  5300  acexmidlem2  5872  acexmid  5874  dfsmo2  6288  smores2  6295  tfrcllemsucaccv  6355  findcard2d  6891  exmidfodomr  7203  acfun  7206  exmidontriimlem3  7222  exmidontriimlem4  7223  exmidontriim  7224  onntri13  7237  exmidontri  7238  onntri51  7239  onntri3or  7244  exmidmotap  7260  ccfunen  7263  cc1  7264  ltsopi  7319  fnn0nninf  10437  fsum2dlemstep  11442  fprod2dlemstep  11630  exmidunben  12427  prdsex  12718  isbasis3g  13549  tgcl  13567  tgss2  13582  blbas  13936  metrest  14009  bdcuni  14631  bdcint  14632  bdcriota  14638  bdsep1  14640  bdsep2  14641  bdsepnft  14642  bdsepnf  14643  bdsepnfALT  14644  bdzfauscl  14645  bdbm1.3ii  14646  bj-axemptylem  14647  bj-axempty  14648  bj-axempty2  14649  bj-nalset  14650  bdinex1  14654  bj-zfpair2  14665  bj-axun2  14670  bj-uniex2  14671  bj-d0clsepcl  14680  bj-nn0suc0  14705  bj-nntrans  14706  bj-omex2  14732  strcollnft  14739  sscoll2  14743  nninfsellemcl  14763  nninfsellemsuc  14764  nninfsellemqall  14767  nninfomni  14771  exmidsbthrlem  14773