Theorem wel 2168

Description: Extend wff definition to include atomic formulas with the membership predicate. This is read either "𝑥 is an element of 𝑦", or "𝑥 is a member of 𝑦", or "𝑥 belongs to 𝑦", or "𝑦 contains 𝑥". Note: The phrase "𝑦 includes 𝑥 " means "𝑥 is a subset of 𝑦"; to use it also for 𝑥 ∈ 𝑦, 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 ∈ 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 ∈ 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 2168 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 2167. This lets us avoid overloading the ∈ connective, thus preventing ambiguity that would complicate certain Metamath parsers. However, logically wel 2168 is considered to be a primitive syntax, even though here it is artificially "derived" from wcel 2167. 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 𝑥 ∈ 𝑦

Proof of Theorem wel

Step	Hyp	Ref	Expression
1		wcel 2167	1 wff 𝑥 ∈ 𝑦

Syntax hints:   ∈ wcel 2167

This theorem is referenced by:  elequ1  2171  elequ2  2172  cleljust  2173  elsb1  2174  elsb2  2175  dveel1  2176  dveel2  2177  axext3  2179  axext4  2180  bm1.1  2181  ru  2988  nfuni  3846  nfunid  3847  unieq  3849  inteq  3878  nfint  3885  uniiun  3971  intiin  3972  trint  4147  axsep2  4153  bm1.3ii  4155  zfnuleu  4158  0ex  4161  nalset  4164  vnex  4165  repizf2  4196  axpweq  4205  zfpow  4209  axpow2  4210  axpow3  4211  el  4212  vpwex  4213  dtruarb  4225  exmidn0m  4235  exmidsssn  4236  fr0  4387  wetrep  4396  zfun  4470  axun2  4471  uniuni  4487  regexmid  4572  zfregfr  4611  ordwe  4613  wessep  4615  nnregexmid  4658  rele  4797  funimaexglem  5342  acexmidlem2  5922  acexmid  5924  dfsmo2  6354  smores2  6361  tfrcllemsucaccv  6421  pw2f1odclem  6904  findcard2d  6961  exmidfodomr  7285  acfun  7292  exmidontriimlem3  7308  exmidontriimlem4  7309  exmidontriim  7310  onntri13  7323  exmidontri  7324  onntri51  7325  onntri3or  7330  exmidmotap  7346  ccfunen  7349  cc1  7350  ltsopi  7406  fnn0nninf  10549  fsum2dlemstep  11618  fprod2dlemstep  11806  exmidunben  12670  prdsex  12973  isbasis3g  14390  tgcl  14408  tgss2  14423  blbas  14777  metrest  14850  dvmptfsum  15069  bdcuni  15630  bdcint  15631  bdcriota  15637  bdsep1  15639  bdsep2  15640  bdsepnft  15641  bdsepnf  15642  bdsepnfALT  15643  bdzfauscl  15644  bdbm1.3ii  15645  bj-axemptylem  15646  bj-axempty  15647  bj-axempty2  15648  bj-nalset  15649  bdinex1  15653  bj-zfpair2  15664  bj-axun2  15669  bj-uniex2  15670  bj-d0clsepcl  15679  bj-nn0suc0  15704  bj-nntrans  15705  bj-omex2  15731  strcollnft  15738  sscoll2  15742  nninfsellemcl  15766  nninfsellemsuc  15767  nninfsellemqall  15770  nninfomni  15774  exmidsbthrlem  15779