Theorem wel 2203

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

Syntax hints:   ∈ wcel 2202

This theorem is referenced by:  elequ1  2206  elequ2  2207  cleljust  2208  elsb1  2209  elsb2  2210  dveel1  2211  dveel2  2212  axext3  2214  axext4  2215  bm1.1  2216  ru  3030  nfuni  3899  nfunid  3900  unieq  3902  inteq  3931  nfint  3938  uniiun  4024  intiin  4025  trint  4202  axsep2  4208  bm1.3ii  4210  zfnuleu  4213  0ex  4216  nalset  4219  vnex  4220  repizf2  4252  axpweq  4261  zfpow  4265  axpow2  4266  axpow3  4267  el  4268  vpwex  4269  dtruarb  4281  exmidn0m  4291  exmidsssn  4292  fr0  4448  wetrep  4457  zfun  4531  axun2  4532  uniuni  4548  regexmid  4633  zfregfr  4672  ordwe  4674  wessep  4676  nnregexmid  4719  rele  4860  funimaexglem  5413  acexmidlem2  6014  acexmid  6016  dfsmo2  6452  smores2  6459  tfrcllemsucaccv  6519  pw2f1odclem  7019  findcard2d  7079  sspw1or2  7402  exmidfodomr  7414  acfun  7421  exmidontriimlem3  7437  exmidontriimlem4  7438  exmidontriim  7439  onntri13  7455  exmidontri  7456  onntri51  7457  onntri3or  7462  exmidmotap  7479  ccfunen  7482  cc1  7483  ltsopi  7539  fnn0nninf  10699  fsum2dlemstep  11994  fprod2dlemstep  12182  exmidunben  13046  prdsex  13351  isbasis3g  14769  tgcl  14787  tgss2  14802  blbas  15156  metrest  15229  dvmptfsum  15448  uhgrfm  15923  ushgrfm  15924  uhgrss  15925  uhgreq12g  15926  uhgrfun  15927  ushgruhgr  15930  isuhgropm  15931  uhgr0e  15932  uhgr0vb  15934  uhgr0  15935  uhgrun  15936  bdcuni  16471  bdcint  16472  bdcriota  16478  bdsep1  16480  bdsep2  16481  bdsepnft  16482  bdsepnf  16483  bdsepnfALT  16484  bdzfauscl  16485  bdbm1.3ii  16486  bj-axemptylem  16487  bj-axempty  16488  bj-axempty2  16489  bj-nalset  16490  bdinex1  16494  bj-zfpair2  16505  bj-axun2  16510  bj-uniex2  16511  bj-d0clsepcl  16520  bj-nn0suc0  16545  bj-nntrans  16546  bj-omex2  16572  strcollnft  16579  sscoll2  16583  nninfsellemcl  16613  nninfsellemsuc  16614  nninfsellemqall  16617  nninfomni  16621  exmidsbthrlem  16626