Theorem fnmptd

Description: The maps-to notation defines a function with domain. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	fnmptd.1	|- F/ x ph
	fnmptd.2	|- ( ( ph /\ x e. A ) -> B e. V )
	fnmptd.3	|- F = ( x e. A |-> B )
Assertion	fnmptd	|- ( ph -> F Fn A )

Proof

Step	Hyp	Ref	Expression
1		fnmptd.1	|- F/ x ph
2		fnmptd.2	|- ( ( ph /\ x e. A ) -> B e. V )
3		fnmptd.3	|- F = ( x e. A |-> B )
4	2	ex	|- ( ph -> ( x e. A -> B e. V ) )
5	1 4	ralrimi	|- ( ph -> A. x e. A B e. V )
6	3	fnmpt	|- ( A. x e. A B e. V -> F Fn A )
7	5 6	syl	|- ( ph -> F Fn A )