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  2961  nfuni  3815  nfunid  3816  unieq  3818  inteq  3847  nfint  3854  uniiun  3940  intiin  3941  trint  4116  axsep2  4122  bm1.3ii  4124  zfnuleu  4127  0ex  4130  nalset  4133  vnex  4134  repizf2  4162  axpweq  4171  zfpow  4175  axpow2  4176  axpow3  4177  el  4178  vpwex  4179  dtruarb  4191  exmidn0m  4201  exmidsssn  4202  fr0  4351  wetrep  4360  zfun  4434  axun2  4435  uniuni  4451  regexmid  4534  zfregfr  4573  ordwe  4575  wessep  4577  nnregexmid  4620  rele  4757  funimaexglem  5299  acexmidlem2  5871  acexmid  5873  dfsmo2  6287  smores2  6294  tfrcllemsucaccv  6354  findcard2d  6890  exmidfodomr  7202  acfun  7205  exmidontriimlem3  7221  exmidontriimlem4  7222  exmidontriim  7223  onntri13  7236  exmidontri  7237  onntri51  7238  onntri3or  7243  exmidmotap  7259  ccfunen  7262  cc1  7263  ltsopi  7318  fnn0nninf  10434  fsum2dlemstep  11437  fprod2dlemstep  11625  exmidunben  12421  prdsex  12712  isbasis3g  13477  tgcl  13495  tgss2  13510  blbas  13864  metrest  13937  bdcuni  14548  bdcint  14549  bdcriota  14555  bdsep1  14557  bdsep2  14558  bdsepnft  14559  bdsepnf  14560  bdsepnfALT  14561  bdzfauscl  14562  bdbm1.3ii  14563  bj-axemptylem  14564  bj-axempty  14565  bj-axempty2  14566  bj-nalset  14567  bdinex1  14571  bj-zfpair2  14582  bj-axun2  14587  bj-uniex2  14588  bj-d0clsepcl  14597  bj-nn0suc0  14622  bj-nntrans  14623  bj-omex2  14649  strcollnft  14656  sscoll2  14660  nninfsellemcl  14680  nninfsellemsuc  14681  nninfsellemqall  14684  nninfomni  14688  exmidsbthrlem  14690