Theorem wel 2204

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

Syntax hints:   ∈ wcel 2203

This theorem is referenced by:  elequ1  2207  elequ2  2208  cleljust  2209  elsb1  2210  elsb2  2211  dveel1  2212  dveel2  2213  axext3  2215  axext4  2216  bm1.1  2217  ru  3041  nfuni  3920  nfunid  3921  unieq  3923  inteq  3952  nfint  3959  uniiun  4045  intiin  4046  trint  4223  axsep2  4229  bm1.3ii  4231  zfnuleu  4234  0ex  4237  nalset  4240  vnex  4241  repizf2  4275  axpweq  4284  zfpow  4288  axpow2  4289  axpow3  4290  el  4291  vpwex  4292  dtruarb  4304  exmidn0m  4314  exmidsssn  4315  fr0  4472  wetrep  4481  zfun  4555  axun2  4556  uniuni  4572  regexmid  4657  zfregfr  4696  ordwe  4698  wessep  4700  nnregexmid  4743  rele  4885  funimaexglem  5439  acexmidlem2  6047  acexmid  6049  dfsmo2  6518  smores2  6525  tfrcllemsucaccv  6585  pw2f1odclem  7087  findcard2d  7148  sspw1or2  7495  exmidfodomr  7507  acfun  7514  exmidontriimlem3  7530  exmidontriimlem4  7531  exmidontriim  7532  onntri13  7548  exmidontri  7549  onntri51  7550  onntri3or  7555  exmidmotap  7575  ccfunen  7578  cc1  7579  ltsopi  7635  fnn0nninf  10800  hashfibclem  11206  fsum2dlemstep  12120  fprod2dlemstep  12308  exmidunben  13177  prdsex  13482  isbasis3g  14911  tgcl  14929  tgss2  14944  blbas  15298  metrest  15371  dvmptfsum  15590  uhgrfm  16068  ushgrfm  16069  uhgrss  16070  uhgreq12g  16071  uhgrfun  16072  ushgruhgr  16075  isuhgropm  16076  uhgr0e  16077  uhgr0vb  16079  uhgr0  16080  uhgrun  16081  bdcuni  16646  bdcint  16647  bdcriota  16653  bdsep1  16655  bdsep2  16656  bdsepnft  16657  bdsepnf  16658  bdsepnfALT  16659  bdzfauscl  16660  bdbm1.3ii  16661  bj-axemptylem  16662  bj-axempty  16663  bj-axempty2  16664  bj-nalset  16665  bdinex1  16669  bj-zfpair2  16680  bj-axun2  16685  bj-uniex2  16686  bj-d0clsepcl  16695  bj-nn0suc0  16720  bj-nntrans  16721  bj-omex2  16747  strcollnft  16754  sscoll2  16758  nninfsellemcl  16789  nninfsellemsuc  16790  nninfsellemqall  16793  nninfomni  16797  exmidsbthrlem  16802