Theorem wel 1301

Description: Extend wff definition to include atomic formulas with the epsilon (membership) predicate. This is read "x is an element of y," "x is a member of y," "x belongs to y," or "y contains x." Note: The phrase "y includes x " means "x is a subset of y;" to use it also for x e. y, 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 e. (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 e. 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 1301 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 1300. This lets us avoid overloading the e. connective, thus preventing ambiguity that would complicate certain Metamath parsers. However, logically wel 1301 is considered to be a primitive syntax, even though here it is artificially "derived" from wcel 1300. Note: To see the proof steps of this syntax proof, type "show proof wel /all" in the Metamath program.)

Assertion

Ref	Expression
wel	wff x e. y

Proof of Theorem wel

Step	Hyp	Ref	Expression
1		wcel 1300	1 wff x e. y

Syntax hints:   e. wcel 1300

This theorem is referenced by:  elequ1 1496  elequ2 1497  cleljust 1713  elsb3 1718  elsb3OLD 1719  elsb4 1720  elsb4OLD 1721  dveel1 1747  dveel2 1748  ax15 1750  ax17el 1752  dveel2ALT 1753  ax11el 1755  truni 3425  trint 3426  trintss 3427  eufnfv 4771  zfregs2 5755  en3lplem1 5756  en3lplem2 5757  en3lp 5758  sbcoreleleq 5830  tratrb 5831  ordelordaxr 5833  trsbc 5843  truniALT 5845  axextprim 13785  axrepprim 13786  axunprim 13787  axpowprim 13788  axregprim 13789  axinfprim 13790  axacprim 13791  truniOLD 13792  trintOLD 13794  trintssOLD 13795  untelirr 13796  untuni 13797  untsucf 13798  unt0 13799  untint 13800  efrunt 13801  untangtr 13802  epelcNEW 13826  dffr5 13831  dftr6 13834  setinds 13844  elpotr 13847  dfon2lem3 13851  dfon2lem4 13852  dfon2lem5 13853  dfon2lem6 13854  dfon2lem7 13855  dfon2lem8 13856  dfon2lem9 13857  dfon2 13858  axextdfeq 13864  ax13dfeq 13865  axextdist 13866  axext4dist 13867  distel 13870  tfisg 13912  trcleq1 13926  trcleq2 13927  trcllem1 13933  frxp 13951  poseq 13954  soseq 13955  wfrlem4 13960  wfrlem12 13968  tfrALTlem 13976  axfelem5 14035  brsset 14069  dfon3 14072  brbigcup 14074  dfom5 14081  surjsec2 14467  hbprod1 14659  hbprod 14660  fprodserzfi 14672  fprod1fi 14675  fprod1slem 14676  fprodp1fi 14680  svli2 14826  fnctartar 15284  fnctartar2 15285  pwtr 16647  pwtrr 16649  suctrALT2 16661  trintALT 16705

Copyright terms: Public domain