Theorem wel 1462

Description: Extend wff definition to include atomic formulas with the epsilon (membership) predicate. This is read "𝑥 is an element of 𝑦," "𝑥 is a member of 𝑦," "𝑥 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 ∈ (epsilon) 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 1462 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 1461. This lets us avoid overloading the ∈ connective, thus preventing ambiguity that would complicate certain Metamath parsers. However, logically wel 1462 is considered to be a primitive syntax, even though here it is artificially "derived" from wcel 1461. Note: To see the proof steps of this syntax proof, type "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 1461	1 wff 𝑥 ∈ 𝑦

Syntax hints:   ∈ wcel 1461

This theorem is referenced by:  elequ1  1671  elequ2  1672  cleljust  1886  elsb3  1925  elsb4  1926  dveel1  1969  dveel2  1970  axext3  2096  axext4  2097  bm1.1  2098  ru  2875  nfuni  3706  nfunid  3707  unieq  3709  inteq  3738  nfint  3745  uniiun  3830  intiin  3831  trint  3999  axsep2  4005  bm1.3ii  4007  zfnuleu  4010  0ex  4013  nalset  4016  vnex  4017  repizf2  4044  axpweq  4053  zfpow  4057  axpow2  4058  axpow3  4059  el  4060  vpwex  4061  dtruarb  4073  exmidn0m  4082  exmidsssn  4083  fr0  4231  wetrep  4240  zfun  4314  axun2  4315  uniuni  4330  regexmid  4408  zfregfr  4446  ordwe  4448  wessep  4450  nnregexmid  4492  rele  4627  funimaexglem  5162  acexmidlem2  5723  acexmid  5725  dfsmo2  6136  smores2  6143  tfrcllemsucaccv  6203  findcard2d  6736  exmidfodomr  7005  acfun  7008  ltsopi  7070  fnn0nninf  10097  fsum2dlemstep  11089  exmidunben  11778  isbasis3g  12050  tgcl  12070  tgss2  12085  blbas  12416  metrest  12489  bdcuni  12757  bdcint  12758  bdcriota  12764  bdsep1  12766  bdsep2  12767  bdsepnft  12768  bdsepnf  12769  bdsepnfALT  12770  bdzfauscl  12771  bdbm1.3ii  12772  bj-axemptylem  12773  bj-axempty  12774  bj-axempty2  12775  bj-nalset  12776  bdinex1  12780  bj-zfpair2  12791  bj-axun2  12796  bj-uniex2  12797  bj-d0clsepcl  12806  bj-nn0suc0  12831  bj-nntrans  12832  bj-omex2  12858  strcoll2  12864  strcollnft  12865  strcollnf  12866  strcollnfALT  12867  sscoll2  12869  nninfsellemcl  12888  nninfsellemsuc  12889  nninfsellemqall  12892  nninfomni  12896  exmidsbthrlem  12898