Theorem mptfnd

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
Hypotheses	mptfnd.1	|- F/_ x A
	mptfnd.2	|- F/ x ph
	mptfnd.3	|- ( ( ph /\ x e. A ) -> B e. V )
Assertion	mptfnd	|- ( ph -> ( x e. A |-> B ) Fn A )

Proof

Step	Hyp	Ref	Expression
1		mptfnd.1	|- F/_ x A
2		mptfnd.2	|- F/ x ph
3		mptfnd.3	|- ( ( ph /\ x e. A ) -> B e. V )
4	3	ex	|- ( ph -> ( x e. A -> B e. V ) )
5		elex	|- ( B e. V -> B e. _V )
6	4 5	syl6	|- ( ph -> ( x e. A -> B e. _V ) )
7	2 6	ralrimi	|- ( ph -> A. x e. A B e. _V )
8	1	mptfnf	|- ( A. x e. A B e. _V <-> ( x e. A |-> B ) Fn A )
9	7 8	sylib	|- ( ph -> ( x e. A |-> B ) Fn A )