Description: Extend wff definition to
include atomic formulas using the equality
predicate.
(Instead of introducing weq 1969 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 wceq 1542. This lets us avoid overloading
the = connective, thus preventing ambiguity that
would complicate
certain Metamath parsers. However, logically weq 1969 is
considered to be a
primitive syntax, even though here it is artificially "derived"
from
wceq 1542. Note: To see the proof steps of this
syntax proof, type "MM>
SHOW PROOF weq / ALL" in the Metamath program.) (Contributed by NM,
24-Jan-2006.) |