Theorem wel 957

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

Syntax hints:   e. wcel 956

This theorem is referenced by:  elequ1 1134  elequ2 1135  cleljust 1326  elsb3 1329  dveel1 1354  dveel2 1355  ax15 1357  ax17el 1359  dveel2ALT 1360  ax11el 1362  cbvrexf 10374  fgsb2 10485  cnfilca 10487

Copyright terms: Public domain