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  3028  nfuni  3897  nfunid  3898  unieq  3900  inteq  3929  nfint  3936  uniiun  4022  intiin  4023  trint  4200  axsep2  4206  bm1.3ii  4208  zfnuleu  4211  0ex  4214  nalset  4217  vnex  4218  repizf2  4250  axpweq  4259  zfpow  4263  axpow2  4264  axpow3  4265  el  4266  vpwex  4267  dtruarb  4279  exmidn0m  4289  exmidsssn  4290  fr0  4446  wetrep  4455  zfun  4529  axun2  4530  uniuni  4546  regexmid  4631  zfregfr  4670  ordwe  4672  wessep  4674  nnregexmid  4717  rele  4858  funimaexglem  5410  acexmidlem2  6010  acexmid  6012  dfsmo2  6448  smores2  6455  tfrcllemsucaccv  6515  pw2f1odclem  7015  findcard2d  7073  exmidfodomr  7405  acfun  7412  exmidontriimlem3  7428  exmidontriimlem4  7429  exmidontriim  7430  onntri13  7446  exmidontri  7447  onntri51  7448  onntri3or  7453  exmidmotap  7470  ccfunen  7473  cc1  7474  ltsopi  7530  fnn0nninf  10690  fsum2dlemstep  11985  fprod2dlemstep  12173  exmidunben  13037  prdsex  13342  isbasis3g  14760  tgcl  14778  tgss2  14793  blbas  15147  metrest  15220  dvmptfsum  15439  uhgrfm  15914  ushgrfm  15915  uhgrss  15916  uhgreq12g  15917  uhgrfun  15918  ushgruhgr  15921  isuhgropm  15922  uhgr0e  15923  uhgr0vb  15925  uhgr0  15926  uhgrun  15927  bdcuni  16407  bdcint  16408  bdcriota  16414  bdsep1  16416  bdsep2  16417  bdsepnft  16418  bdsepnf  16419  bdsepnfALT  16420  bdzfauscl  16421  bdbm1.3ii  16422  bj-axemptylem  16423  bj-axempty  16424  bj-axempty2  16425  bj-nalset  16426  bdinex1  16430  bj-zfpair2  16441  bj-axun2  16446  bj-uniex2  16447  bj-d0clsepcl  16456  bj-nn0suc0  16481  bj-nntrans  16482  bj-omex2  16508  strcollnft  16515  sscoll2  16519  nninfsellemcl  16549  nninfsellemsuc  16550  nninfsellemqall  16553  nninfomni  16557  exmidsbthrlem  16562