Description: Extend wff definition to include atomic formulas using the equality predicate.
(Instead of introducing weq 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 . This lets us avoid overloading the = connective, thus preventing ambiguity that would complicate certain Metamath parsers. However, logically weq is considered to be a primitive syntax, even though here it is artificially "derived" from wceq . 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)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | weq | wff x = y |