Metamath Proof Explorer


Syntax definition word

Description: Extend the definition of a wff to include the ordinal predicate.

Ref Expression
Assertion word wff Ord A