Theorem wel 2210

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

Syntax hints:   ∈ wcel 2209

This theorem is referenced by:  elequ1  2213  elequ2  2214  cleljust  2215  elsb1  2216  elsb2  2217  dveel1  2218  dveel2  2219  axext3  2221  axext4  2222  bm1.1  2223  ru  3050  nfuni  3936  nfunid  3937  unieq  3939  inteq  3968  nfint  3975  uniiun  4061  intiin  4062  trint  4239  axsepg  4245  sepg  4246  sepgi  4247  bm1.3ii  4249  zfnuleu  4252  0ex  4255  nalset  4258  vnex  4259  repizf2  4294  axpweq  4303  zfpow  4307  axpow2  4308  axpow3  4309  el  4310  vpwex  4311  dtruarb  4323  exmidn0m  4333  exmidsssn  4334  fr0  4491  wetrep  4500  zfun  4574  axun2  4575  uniex2  4576  uniuni  4592  regexmid  4677  zfregfr  4716  ordwe  4718  wessep  4720  nnregexmid  4763  rele  4905  funimaexglem  5459  acexmidlem2  6072  acexmid  6074  dfsmo2  6548  smores2  6555  tfrcllemsucaccv  6615  pw2f1odclem  7124  findcard2d  7185  sspw1or2  7534  exmidfodomr  7546  acfun  7553  exmidontriimlem3  7569  exmidontriimlem4  7570  exmidontriim  7571  onntri13  7587  exmidontri  7588  onntri51  7589  onntri3or  7594  exmidmotap  7617  ccfunen  7620  cc1  7621  ltsopi  7677  fnn0nninf  10853  hashfibclem  11260  fsum2dlemstep  12179  fprod2dlemstep  12367  exmidunben  13295  prdsex  14149  isbasis3g  15070  tgcl  15088  tgss2  15103  blbas  15457  metrest  15530  dvmptfsum  15749  uhgrfm  16228  ushgrfm  16229  uhgrss  16230  uhgreq12g  16231  uhgrfun  16232  ushgruhgr  16235  isuhgropm  16236  uhgr0e  16237  uhgr0vb  16239  uhgr0  16240  uhgrun  16241  bdcuni  16816  bdcint  16817  bdcriota  16823  bdsep1  16825  bdsep2  16826  bdsepnft  16827  bdsepnf  16828  bdsepnfALT  16829  bdsepg  16830  bdbm1.3ii  16831  bj-axemptylem  16832  bj-axempty  16833  bj-axempty2  16834  bj-nalset  16835  bdinex1  16839  bj-zfpair2  16850  bj-axun2  16855  bj-uniex2  16856  bj-d0clsepcl  16865  bj-nn0suc0  16890  bj-nntrans  16891  bj-omex2  16917  strcollnft  16924  sscoll2  16928  nninfsellemcl  16959  nninfsellemsuc  16960  nninfsellemqall  16963  nninfomni  16967  exmidsbthrlem  16972