Theorem fnmptf

Description: The maps-to notation defines a function with domain. (Contributed by NM, 9-Apr-2013) (Revised by Thierry Arnoux, 10-May-2017)

	Ref	Expression
Hypothesis	mptfnf.0	|- F/_ x A
Assertion	fnmptf	|- ( A. x e. A B e. V -> ( x e. A |-> B ) Fn A )

Proof

Step	Hyp	Ref	Expression
1		mptfnf.0	|- F/_ x A
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	mptfnf	|- ( A. x e. A B e. _V <-> ( x e. A |-> B ) Fn A )
5	3 4	sylib	|- ( A. x e. A B e. V -> ( x e. A |-> B ) Fn A )