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  6015  acexmid  6017  dfsmo2  6453  smores2  6460  tfrcllemsucaccv  6520  pw2f1odclem  7020  findcard2d  7080  sspw1or2  7403  exmidfodomr  7415  acfun  7422  exmidontriimlem3  7438  exmidontriimlem4  7439  exmidontriim  7440  onntri13  7456  exmidontri  7457  onntri51  7458  onntri3or  7463  exmidmotap  7480  ccfunen  7483  cc1  7484  ltsopi  7540  fnn0nninf  10701  fsum2dlemstep  12013  fprod2dlemstep  12201  exmidunben  13065  prdsex  13370  isbasis3g  14789  tgcl  14807  tgss2  14822  blbas  15176  metrest  15249  dvmptfsum  15468  uhgrfm  15943  ushgrfm  15944  uhgrss  15945  uhgreq12g  15946  uhgrfun  15947  ushgruhgr  15950  isuhgropm  15951  uhgr0e  15952  uhgr0vb  15954  uhgr0  15955  uhgrun  15956  bdcuni  16522  bdcint  16523  bdcriota  16529  bdsep1  16531  bdsep2  16532  bdsepnft  16533  bdsepnf  16534  bdsepnfALT  16535  bdzfauscl  16536  bdbm1.3ii  16537  bj-axemptylem  16538  bj-axempty  16539  bj-axempty2  16540  bj-nalset  16541  bdinex1  16545  bj-zfpair2  16556  bj-axun2  16561  bj-uniex2  16562  bj-d0clsepcl  16571  bj-nn0suc0  16596  bj-nntrans  16597  bj-omex2  16623  strcollnft  16630  sscoll2  16634  nninfsellemcl  16664  nninfsellemsuc  16665  nninfsellemqall  16668  nninfomni  16672  exmidsbthrlem  16677