Theorem wel 2206

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

Syntax hints:   ∈ wcel 2205

This theorem is referenced by:  elequ1  2209  elequ2  2210  cleljust  2211  elsb1  2212  elsb2  2213  dveel1  2214  dveel2  2215  axext3  2217  axext4  2218  bm1.1  2219  ru  3044  nfuni  3925  nfunid  3926  unieq  3928  inteq  3957  nfint  3964  uniiun  4050  intiin  4051  trint  4228  axsep2  4234  bm1.3ii  4236  zfnuleu  4239  0ex  4242  nalset  4245  vnex  4246  repizf2  4280  axpweq  4289  zfpow  4293  axpow2  4294  axpow3  4295  el  4296  vpwex  4297  dtruarb  4309  exmidn0m  4319  exmidsssn  4320  fr0  4477  wetrep  4486  zfun  4560  axun2  4561  uniuni  4577  regexmid  4662  zfregfr  4701  ordwe  4703  wessep  4705  nnregexmid  4748  rele  4890  funimaexglem  5444  acexmidlem2  6055  acexmid  6057  dfsmo2  6531  smores2  6538  tfrcllemsucaccv  6598  pw2f1odclem  7100  findcard2d  7161  sspw1or2  7508  exmidfodomr  7520  acfun  7527  exmidontriimlem3  7543  exmidontriimlem4  7544  exmidontriim  7545  onntri13  7561  exmidontri  7562  onntri51  7563  onntri3or  7568  exmidmotap  7591  ccfunen  7594  cc1  7595  ltsopi  7651  fnn0nninf  10824  hashfibclem  11231  fsum2dlemstep  12145  fprod2dlemstep  12333  exmidunben  13261  prdsex  14114  isbasis3g  15037  tgcl  15055  tgss2  15070  blbas  15424  metrest  15497  dvmptfsum  15716  uhgrfm  16194  ushgrfm  16195  uhgrss  16196  uhgreq12g  16197  uhgrfun  16198  ushgruhgr  16201  isuhgropm  16202  uhgr0e  16203  uhgr0vb  16205  uhgr0  16206  uhgrun  16207  bdcuni  16772  bdcint  16773  bdcriota  16779  bdsep1  16781  bdsep2  16782  bdsepnft  16783  bdsepnf  16784  bdsepnfALT  16785  bdzfauscl  16786  bdbm1.3ii  16787  bj-axemptylem  16788  bj-axempty  16789  bj-axempty2  16790  bj-nalset  16791  bdinex1  16795  bj-zfpair2  16806  bj-axun2  16811  bj-uniex2  16812  bj-d0clsepcl  16821  bj-nn0suc0  16846  bj-nntrans  16847  bj-omex2  16873  strcollnft  16880  sscoll2  16884  nninfsellemcl  16915  nninfsellemsuc  16916  nninfsellemqall  16919  nninfomni  16923  exmidsbthrlem  16928