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  3893  nfunid  3894  unieq  3896  inteq  3925  nfint  3932  uniiun  4018  intiin  4019  trint  4196  axsep2  4202  bm1.3ii  4204  zfnuleu  4207  0ex  4210  nalset  4213  vnex  4214  repizf2  4245  axpweq  4254  zfpow  4258  axpow2  4259  axpow3  4260  el  4261  vpwex  4262  dtruarb  4274  exmidn0m  4284  exmidsssn  4285  fr0  4441  wetrep  4450  zfun  4524  axun2  4525  uniuni  4541  regexmid  4626  zfregfr  4665  ordwe  4667  wessep  4669  nnregexmid  4712  rele  4851  funimaexglem  5403  acexmidlem2  5997  acexmid  5999  dfsmo2  6431  smores2  6438  tfrcllemsucaccv  6498  pw2f1odclem  6991  findcard2d  7049  exmidfodomr  7378  acfun  7385  exmidontriimlem3  7401  exmidontriimlem4  7402  exmidontriim  7403  onntri13  7419  exmidontri  7420  onntri51  7421  onntri3or  7426  exmidmotap  7443  ccfunen  7446  cc1  7447  ltsopi  7503  fnn0nninf  10655  fsum2dlemstep  11940  fprod2dlemstep  12128  exmidunben  12992  prdsex  13297  isbasis3g  14714  tgcl  14732  tgss2  14747  blbas  15101  metrest  15174  dvmptfsum  15393  uhgrfm  15867  ushgrfm  15868  uhgrss  15869  uhgreq12g  15870  uhgrfun  15871  ushgruhgr  15874  isuhgropm  15875  uhgr0e  15876  uhgr0vb  15878  uhgr0  15879  uhgrun  15880  bdcuni  16197  bdcint  16198  bdcriota  16204  bdsep1  16206  bdsep2  16207  bdsepnft  16208  bdsepnf  16209  bdsepnfALT  16210  bdzfauscl  16211  bdbm1.3ii  16212  bj-axemptylem  16213  bj-axempty  16214  bj-axempty2  16215  bj-nalset  16216  bdinex1  16220  bj-zfpair2  16231  bj-axun2  16236  bj-uniex2  16237  bj-d0clsepcl  16246  bj-nn0suc0  16271  bj-nntrans  16272  bj-omex2  16298  strcollnft  16305  sscoll2  16309  nninfsellemcl  16336  nninfsellemsuc  16337  nninfsellemqall  16340  nninfomni  16344  exmidsbthrlem  16349