Theorem wel 2210

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

This proof depends on syntax axioms:   e. wcel 2209

This theorem is used by:  elequ1  2213  elequ2  2214  cleljust  2215  elsb1  2216  elsb2  2217  dveel1  2218  dveel2  2219  axext3  2221  axext4  2222  bm1.1  2223  ru  3050  nfuni  3941  nfunid  3942  unieq  3944  inteq  3973  nfint  3980  uniiun  4066  intiin  4067  trint  4244  axsepg  4250  sepg  4251  sepgi  4252  bm1.3ii  4254  zfnuleu  4257  0ex  4260  nalset  4263  vnex  4264  repizf2  4299  axpweq  4308  zfpow  4312  axpow2  4313  axpow3  4314  el  4315  vpwex  4316  dtruarb  4328  exmidn0m  4338  exmidsssn  4339  fr0  4496  wetrep  4505  zfun  4579  axun2  4580  uniex2  4581  uniuni  4597  regexmid  4682  zfregfr  4721  ordwe  4723  wessep  4725  nnregexmid  4768  rele  4910  funimaexglem  5464  acexmidlem2  6082  acexmid  6084  dfsmo2  6558  smores2  6565  tfrcllemsucaccv  6625  pw2f1odclem  7134  findcard2d  7195  sspw1or2  7545  exmidfodomr  7557  acfun  7564  exmidontriimlem3  7580  exmidontriimlem4  7581  exmidontriim  7582  onntri13  7598  exmidontri  7599  onntri51  7600  onntri3or  7605  exmidmotap  7628  ccfunen  7631  cc1  7632  ltsopi  7688  fnn0nninf  10890  hashfibclem  11298  fsum2dlemstep  12220  fprod2dlemstep  12408  exmidunben  13369  prdsex  14256  isbasis3g  15238  tgcl  15256  tgss2  15271  blbas  15625  metrest  15698  dvmptfsum  15917  uhgrfm  16480  ushgrfm  16481  uhgrss  16482  uhgreq12g  16483  uhgrfun  16484  ushgruhgr  16487  isuhgropm  16488  uhgr0e  16489  uhgr0vb  16491  uhgr0  16492  uhgrun  16493  bdcuni  17068  bdcint  17069  bdcriota  17075  bdsep1  17077  bdsep2  17078  bdsepnft  17079  bdsepnf  17080  bdsepnfALT  17081  bdsepg  17082  bdbm1.3ii  17083  bj-axemptylem  17084  bj-axempty  17085  bj-axempty2  17086  bj-nalset  17087  bdinex1  17091  bj-zfpair2  17102  bj-axun2  17107  bj-uniex2  17108  bj-d0clsepcl  17117  bj-nn0suc0  17142  bj-nntrans  17143  bj-omex2  17169  strcollnft  17176  sscoll2  17180  nninfsellemcl  17220  nninfsellemsuc  17221  nninfsellemqall  17224  nninfomni  17228  exmidsbthrlem  17233