Theorem wel 2149

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

Syntax hints:   ∈ wcel 2148

This theorem is referenced by:  elequ1  2152  elequ2  2153  cleljust  2154  elsb1  2155  elsb2  2156  dveel1  2157  dveel2  2158  axext3  2160  axext4  2161  bm1.1  2162  ru  2963  nfuni  3817  nfunid  3818  unieq  3820  inteq  3849  nfint  3856  uniiun  3942  intiin  3943  trint  4118  axsep2  4124  bm1.3ii  4126  zfnuleu  4129  0ex  4132  nalset  4135  vnex  4136  repizf2  4164  axpweq  4173  zfpow  4177  axpow2  4178  axpow3  4179  el  4180  vpwex  4181  dtruarb  4193  exmidn0m  4203  exmidsssn  4204  fr0  4353  wetrep  4362  zfun  4436  axun2  4437  uniuni  4453  regexmid  4536  zfregfr  4575  ordwe  4577  wessep  4579  nnregexmid  4622  rele  4759  funimaexglem  5301  acexmidlem2  5874  acexmid  5876  dfsmo2  6290  smores2  6297  tfrcllemsucaccv  6357  findcard2d  6893  exmidfodomr  7205  acfun  7208  exmidontriimlem3  7224  exmidontriimlem4  7225  exmidontriim  7226  onntri13  7239  exmidontri  7240  onntri51  7241  onntri3or  7246  exmidmotap  7262  ccfunen  7265  cc1  7266  ltsopi  7321  fnn0nninf  10439  fsum2dlemstep  11444  fprod2dlemstep  11632  exmidunben  12429  prdsex  12723  isbasis3g  13631  tgcl  13649  tgss2  13664  blbas  14018  metrest  14091  bdcuni  14713  bdcint  14714  bdcriota  14720  bdsep1  14722  bdsep2  14723  bdsepnft  14724  bdsepnf  14725  bdsepnfALT  14726  bdzfauscl  14727  bdbm1.3ii  14728  bj-axemptylem  14729  bj-axempty  14730  bj-axempty2  14731  bj-nalset  14732  bdinex1  14736  bj-zfpair2  14747  bj-axun2  14752  bj-uniex2  14753  bj-d0clsepcl  14762  bj-nn0suc0  14787  bj-nntrans  14788  bj-omex2  14814  strcollnft  14821  sscoll2  14825  nninfsellemcl  14845  nninfsellemsuc  14846  nninfsellemqall  14849  nninfomni  14853  exmidsbthrlem  14855