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  3031  nfuni  3904  nfunid  3905  unieq  3907  inteq  3936  nfint  3943  uniiun  4029  intiin  4030  trint  4207  axsep2  4213  bm1.3ii  4215  zfnuleu  4218  0ex  4221  nalset  4224  vnex  4225  repizf2  4258  axpweq  4267  zfpow  4271  axpow2  4272  axpow3  4273  el  4274  vpwex  4275  dtruarb  4287  exmidn0m  4297  exmidsssn  4298  fr0  4454  wetrep  4463  zfun  4537  axun2  4538  uniuni  4554  regexmid  4639  zfregfr  4678  ordwe  4680  wessep  4682  nnregexmid  4725  rele  4866  funimaexglem  5420  acexmidlem2  6025  acexmid  6027  dfsmo2  6496  smores2  6503  tfrcllemsucaccv  6563  pw2f1odclem  7063  findcard2d  7123  sspw1or2  7463  exmidfodomr  7475  acfun  7482  exmidontriimlem3  7498  exmidontriimlem4  7499  exmidontriim  7500  onntri13  7516  exmidontri  7517  onntri51  7518  onntri3or  7523  exmidmotap  7540  ccfunen  7543  cc1  7544  ltsopi  7600  fnn0nninf  10763  fsum2dlemstep  12075  fprod2dlemstep  12263  exmidunben  13127  prdsex  13432  isbasis3g  14857  tgcl  14875  tgss2  14890  blbas  15244  metrest  15317  dvmptfsum  15536  uhgrfm  16014  ushgrfm  16015  uhgrss  16016  uhgreq12g  16017  uhgrfun  16018  ushgruhgr  16021  isuhgropm  16022  uhgr0e  16023  uhgr0vb  16025  uhgr0  16026  uhgrun  16027  bdcuni  16592  bdcint  16593  bdcriota  16599  bdsep1  16601  bdsep2  16602  bdsepnft  16603  bdsepnf  16604  bdsepnfALT  16605  bdzfauscl  16606  bdbm1.3ii  16607  bj-axemptylem  16608  bj-axempty  16609  bj-axempty2  16610  bj-nalset  16611  bdinex1  16615  bj-zfpair2  16626  bj-axun2  16631  bj-uniex2  16632  bj-d0clsepcl  16641  bj-nn0suc0  16666  bj-nntrans  16667  bj-omex2  16693  strcollnft  16700  sscoll2  16704  nninfsellemcl  16737  nninfsellemsuc  16738  nninfsellemqall  16741  nninfomni  16745  exmidsbthrlem  16750