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