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  7283  acfun  7290  exmidontriimlem3  7306  exmidontriimlem4  7307  exmidontriim  7308  onntri13  7321  exmidontri  7322  onntri51  7323  onntri3or  7328  exmidmotap  7344  ccfunen  7347  cc1  7348  ltsopi  7404  fnn0nninf  10547  fsum2dlemstep  11616  fprod2dlemstep  11804  exmidunben  12668  prdsex  12971  isbasis3g  14366  tgcl  14384  tgss2  14399  blbas  14753  metrest  14826  dvmptfsum  15045  bdcuni  15606  bdcint  15607  bdcriota  15613  bdsep1  15615  bdsep2  15616  bdsepnft  15617  bdsepnf  15618  bdsepnfALT  15619  bdzfauscl  15620  bdbm1.3ii  15621  bj-axemptylem  15622  bj-axempty  15623  bj-axempty2  15624  bj-nalset  15625  bdinex1  15629  bj-zfpair2  15640  bj-axun2  15645  bj-uniex2  15646  bj-d0clsepcl  15655  bj-nn0suc0  15680  bj-nntrans  15681  bj-omex2  15707  strcollnft  15714  sscoll2  15718  nninfsellemcl  15742  nninfsellemsuc  15743  nninfsellemqall  15746  nninfomni  15750  exmidsbthrlem  15753