Metamath Proof Explorer


Syntax definition wfun

Description: Extend the definition of a wff to include the function predicate. (Read: A is a function.)

Ref Expression
Assertion wfun
wff Fun A