Syntax definition wf1

Description: Extend the definition of a wff to include one-to-one functions. (Read: F maps A one-to-one into B .) The notation ("1-1" above the arrow) is from Definition 6.15(5) of TakeutiZaring p. 27.

	Ref	Expression
Assertion	wf1	wff F : A -1-1-> B