Theorem wel 2165

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

Syntax hints:   ∈ wcel 2164

This theorem is referenced by:  elequ1  2168  elequ2  2169  cleljust  2170  elsb1  2171  elsb2  2172  dveel1  2173  dveel2  2174  axext3  2176  axext4  2177  bm1.1  2178  ru  2984  nfuni  3841  nfunid  3842  unieq  3844  inteq  3873  nfint  3880  uniiun  3966  intiin  3967  trint  4142  axsep2  4148  bm1.3ii  4150  zfnuleu  4153  0ex  4156  nalset  4159  vnex  4160  repizf2  4191  axpweq  4200  zfpow  4204  axpow2  4205  axpow3  4206  el  4207  vpwex  4208  dtruarb  4220  exmidn0m  4230  exmidsssn  4231  fr0  4382  wetrep  4391  zfun  4465  axun2  4466  uniuni  4482  regexmid  4567  zfregfr  4606  ordwe  4608  wessep  4610  nnregexmid  4653  rele  4792  funimaexglem  5337  acexmidlem2  5915  acexmid  5917  dfsmo2  6340  smores2  6347  tfrcllemsucaccv  6407  pw2f1odclem  6890  findcard2d  6947  exmidfodomr  7264  acfun  7267  exmidontriimlem3  7283  exmidontriimlem4  7284  exmidontriim  7285  onntri13  7298  exmidontri  7299  onntri51  7300  onntri3or  7305  exmidmotap  7321  ccfunen  7324  cc1  7325  ltsopi  7380  fnn0nninf  10509  fsum2dlemstep  11577  fprod2dlemstep  11765  exmidunben  12583  prdsex  12880  isbasis3g  14214  tgcl  14232  tgss2  14247  blbas  14601  metrest  14674  bdcuni  15368  bdcint  15369  bdcriota  15375  bdsep1  15377  bdsep2  15378  bdsepnft  15379  bdsepnf  15380  bdsepnfALT  15381  bdzfauscl  15382  bdbm1.3ii  15383  bj-axemptylem  15384  bj-axempty  15385  bj-axempty2  15386  bj-nalset  15387  bdinex1  15391  bj-zfpair2  15402  bj-axun2  15407  bj-uniex2  15408  bj-d0clsepcl  15417  bj-nn0suc0  15442  bj-nntrans  15443  bj-omex2  15469  strcollnft  15476  sscoll2  15480  nninfsellemcl  15501  nninfsellemsuc  15502  nninfsellemqall  15505  nninfomni  15509  exmidsbthrlem  15512