Theorem wel 2201

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

Syntax hints:   ∈ wcel 2200

This theorem is referenced by:  elequ1  2204  elequ2  2205  cleljust  2206  elsb1  2207  elsb2  2208  dveel1  2209  dveel2  2210  axext3  2212  axext4  2213  bm1.1  2214  ru  3027  nfuni  3894  nfunid  3895  unieq  3897  inteq  3926  nfint  3933  uniiun  4019  intiin  4020  trint  4197  axsep2  4203  bm1.3ii  4205  zfnuleu  4208  0ex  4211  nalset  4214  vnex  4215  repizf2  4246  axpweq  4255  zfpow  4259  axpow2  4260  axpow3  4261  el  4262  vpwex  4263  dtruarb  4275  exmidn0m  4285  exmidsssn  4286  fr0  4442  wetrep  4451  zfun  4525  axun2  4526  uniuni  4542  regexmid  4627  zfregfr  4666  ordwe  4668  wessep  4670  nnregexmid  4713  rele  4852  funimaexglem  5404  acexmidlem2  6004  acexmid  6006  dfsmo2  6439  smores2  6446  tfrcllemsucaccv  6506  pw2f1odclem  7003  findcard2d  7061  exmidfodomr  7393  acfun  7400  exmidontriimlem3  7416  exmidontriimlem4  7417  exmidontriim  7418  onntri13  7434  exmidontri  7435  onntri51  7436  onntri3or  7441  exmidmotap  7458  ccfunen  7461  cc1  7462  ltsopi  7518  fnn0nninf  10672  fsum2dlemstep  11960  fprod2dlemstep  12148  exmidunben  13012  prdsex  13317  isbasis3g  14735  tgcl  14753  tgss2  14768  blbas  15122  metrest  15195  dvmptfsum  15414  uhgrfm  15888  ushgrfm  15889  uhgrss  15890  uhgreq12g  15891  uhgrfun  15892  ushgruhgr  15895  isuhgropm  15896  uhgr0e  15897  uhgr0vb  15899  uhgr0  15900  uhgrun  15901  bdcuni  16294  bdcint  16295  bdcriota  16301  bdsep1  16303  bdsep2  16304  bdsepnft  16305  bdsepnf  16306  bdsepnfALT  16307  bdzfauscl  16308  bdbm1.3ii  16309  bj-axemptylem  16310  bj-axempty  16311  bj-axempty2  16312  bj-nalset  16313  bdinex1  16317  bj-zfpair2  16328  bj-axun2  16333  bj-uniex2  16334  bj-d0clsepcl  16343  bj-nn0suc0  16368  bj-nntrans  16369  bj-omex2  16395  strcollnft  16402  sscoll2  16406  nninfsellemcl  16437  nninfsellemsuc  16438  nninfsellemqall  16441  nninfomni  16445  exmidsbthrlem  16450