Metamath Proof Explorer


Syntax definition wf

Description: Extend the definition of a wff to include the function predicate with domain and codomain. (Read: F maps A into B .)

Ref Expression
Assertion wf
wff F : A --> B