Theorem fmpti

Description: Functionality of the mapping operation. (Contributed by NM, 19-Mar-2005) (Revised by Mario Carneiro, 1-Sep-2015)

	Ref	Expression
Hypotheses	fmpt.1	|- F = ( x e. A |-> C )
	fmpti.2	|- ( x e. A -> C e. B )
Assertion	fmpti	|- F : A --> B

Proof

Step	Hyp	Ref	Expression
1		fmpt.1	|- F = ( x e. A |-> C )
2		fmpti.2	|- ( x e. A -> C e. B )
3	2	rgen	|- A. x e. A C e. B
4	1	fmpt	|- ( A. x e. A C e. B <-> F : A --> B )
5	3 4	mpbi	|- F : A --> B