Theorem wel 2179

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

Syntax hints:   e. wcel 2178

This theorem is referenced by:  elequ1  2182  elequ2  2183  cleljust  2184  elsb1  2185  elsb2  2186  dveel1  2187  dveel2  2188  axext3  2190  axext4  2191  bm1.1  2192  ru  3004  nfuni  3870  nfunid  3871  unieq  3873  inteq  3902  nfint  3909  uniiun  3995  intiin  3996  trint  4173  axsep2  4179  bm1.3ii  4181  zfnuleu  4184  0ex  4187  nalset  4190  vnex  4191  repizf2  4222  axpweq  4231  zfpow  4235  axpow2  4236  axpow3  4237  el  4238  vpwex  4239  dtruarb  4251  exmidn0m  4261  exmidsssn  4262  fr0  4416  wetrep  4425  zfun  4499  axun2  4500  uniuni  4516  regexmid  4601  zfregfr  4640  ordwe  4642  wessep  4644  nnregexmid  4687  rele  4826  funimaexglem  5376  acexmidlem2  5964  acexmid  5966  dfsmo2  6396  smores2  6403  tfrcllemsucaccv  6463  pw2f1odclem  6956  findcard2d  7014  exmidfodomr  7343  acfun  7350  exmidontriimlem3  7366  exmidontriimlem4  7367  exmidontriim  7368  onntri13  7384  exmidontri  7385  onntri51  7386  onntri3or  7391  exmidmotap  7408  ccfunen  7411  cc1  7412  ltsopi  7468  fnn0nninf  10620  fsum2dlemstep  11860  fprod2dlemstep  12048  exmidunben  12912  prdsex  13216  isbasis3g  14633  tgcl  14651  tgss2  14666  blbas  15020  metrest  15093  dvmptfsum  15312  uhgrfm  15784  ushgrfm  15785  uhgrss  15786  uhgreq12g  15787  uhgrfun  15788  ushgruhgr  15791  isuhgropm  15792  uhgr0e  15793  uhgr0vb  15795  uhgr0  15796  uhgrun  15797  bdcuni  16011  bdcint  16012  bdcriota  16018  bdsep1  16020  bdsep2  16021  bdsepnft  16022  bdsepnf  16023  bdsepnfALT  16024  bdzfauscl  16025  bdbm1.3ii  16026  bj-axemptylem  16027  bj-axempty  16028  bj-axempty2  16029  bj-nalset  16030  bdinex1  16034  bj-zfpair2  16045  bj-axun2  16050  bj-uniex2  16051  bj-d0clsepcl  16060  bj-nn0suc0  16085  bj-nntrans  16086  bj-omex2  16112  strcollnft  16119  sscoll2  16123  nninfsellemcl  16150  nninfsellemsuc  16151  nninfsellemqall  16154  nninfomni  16158  exmidsbthrlem  16163