Theorem fmptd

Description: Domain and codomain of the mapping operation; deduction form. (Contributed by Mario Carneiro, 13-Jan-2013)

	Ref	Expression
Hypotheses	fmptd.1	|- ( ( ph /\ x e. A ) -> B e. C )
	fmptd.2	|- F = ( x e. A |-> B )
Assertion	fmptd	|- ( ph -> F : A --> C )

Proof

Step	Hyp	Ref	Expression
1		fmptd.1	|- ( ( ph /\ x e. A ) -> B e. C )
2		fmptd.2	|- F = ( x e. A |-> B )
3	1	ralrimiva	|- ( ph -> A. x e. A B e. C )
4	2	fmpt	|- ( A. x e. A B e. C <-> F : A --> C )
5	3 4	sylib	|- ( ph -> F : A --> C )