Theorem wel 1434

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

Syntax hints:   ∈ wcel 1433

This theorem is referenced by:  elequ1  1640  elequ2  1641  cleljust  1854  elsb3  1893  elsb4  1894  dveel1  1937  dveel2  1938  axext3  2064  axext4  2065  bm1.1  2066  ru  2814  nfuni  3607  nfunid  3608  unieq  3610  inteq  3639  nfint  3646  uniiun  3731  intiin  3732  trint  3890  axsep2  3897  bm1.3ii  3899  zfnuleu  3902  0ex  3905  nalset  3908  repizf2  3936  axpweq  3945  zfpow  3949  axpow2  3950  axpow3  3951  el  3952  dtruarb  3962  fr0  4106  wetrep  4115  zfun  4189  axun2  4190  uniuni  4201  regexmid  4278  zfregfr  4316  ordwe  4318  wessep  4320  nnregexmid  4360  rele  4484  funimaexglem  5002  acexmidlem2  5529  acexmid  5531  dfsmo2  5925  smores2  5932  findcard2d  6375  ltsopi  6510  bdcuni  10667  bdcint  10668  bdcriota  10674  bdsep1  10676  bdsep2  10677  bdsepnft  10678  bdsepnf  10679  bdsepnfALT  10680  bdzfauscl  10681  bdbm1.3ii  10682  bj-axemptylem  10683  bj-axempty  10684  bj-axempty2  10685  bj-nalset  10686  bdinex1  10690  bj-zfpair2  10701  bj-axun2  10706  bj-uniex2  10707  bj-d0clsepcl  10720  bj-nn0suc0  10745  bj-nntrans  10746  bj-omex2  10772  strcoll2  10778  strcollnft  10779  strcollnf  10780  strcollnfALT  10781  sscoll2  10783