Theorem wel 2129

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

Syntax hints:   ∈ wcel 2128

This theorem is referenced by:  elequ1  2132  elequ2  2133  cleljust  2134  elsb3  2135  elsb4  2136  dveel1  2137  dveel2  2138  axext3  2140  axext4  2141  bm1.1  2142  ru  2936  nfuni  3778  nfunid  3779  unieq  3781  inteq  3810  nfint  3817  uniiun  3902  intiin  3903  trint  4077  axsep2  4083  bm1.3ii  4085  zfnuleu  4088  0ex  4091  nalset  4094  vnex  4095  repizf2  4123  axpweq  4132  zfpow  4136  axpow2  4137  axpow3  4138  el  4139  vpwex  4140  dtruarb  4152  exmidn0m  4162  exmidsssn  4163  fr0  4311  wetrep  4320  zfun  4394  axun2  4395  uniuni  4410  regexmid  4493  zfregfr  4532  ordwe  4534  wessep  4536  nnregexmid  4579  rele  4715  funimaexglem  5252  acexmidlem2  5818  acexmid  5820  dfsmo2  6231  smores2  6238  tfrcllemsucaccv  6298  findcard2d  6833  exmidfodomr  7133  acfun  7136  exmidontriimlem3  7152  exmidontriimlem4  7153  exmidontriim  7154  onntri13  7167  exmidontri  7168  onntri51  7169  onntri3or  7174  ccfunen  7178  cc1  7179  ltsopi  7234  fnn0nninf  10329  fsum2dlemstep  11324  fprod2dlemstep  11512  exmidunben  12138  isbasis3g  12415  tgcl  12435  tgss2  12450  blbas  12804  metrest  12877  bdcuni  13422  bdcint  13423  bdcriota  13429  bdsep1  13431  bdsep2  13432  bdsepnft  13433  bdsepnf  13434  bdsepnfALT  13435  bdzfauscl  13436  bdbm1.3ii  13437  bj-axemptylem  13438  bj-axempty  13439  bj-axempty2  13440  bj-nalset  13441  bdinex1  13445  bj-zfpair2  13456  bj-axun2  13461  bj-uniex2  13462  bj-d0clsepcl  13471  bj-nn0suc0  13496  bj-nntrans  13497  bj-omex2  13523  strcollnft  13530  sscoll2  13534  nninfsellemcl  13554  nninfsellemsuc  13555  nninfsellemqall  13558  nninfomni  13562  exmidsbthrlem  13564