Theorem fnmpt

Description: The maps-to notation defines a function with domain. (Contributed by NM, 9-Apr-2013)

	Ref	Expression
Hypothesis	mptfng.1	|- F = ( x e. A |-> B )
Assertion	fnmpt	|- ( A. x e. A B e. V -> F Fn A )

Proof

Step	Hyp	Ref	Expression
1		mptfng.1	|- F = ( x e. A |-> B )
2		elex	|- ( B e. V -> B e. _V )
3	2	ralimi	|- ( A. x e. A B e. V -> A. x e. A B e. _V )
4	1	mptfng	|- ( A. x e. A B e. _V <-> F Fn A )
5	3 4	sylib	|- ( A. x e. A B e. V -> F Fn A )