Metamath Proof Explorer


Syntax definition wfn

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

Ref Expression
Assertion wfn wff A Fn B