Theorem ffnd

Description: A mapping is a function with domain, deduction form. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypothesis	ffnd.1	|- ( ph -> F : A --> B )
Assertion	ffnd	|- ( ph -> F Fn A )

Proof

Step	Hyp	Ref	Expression
1		ffnd.1	|- ( ph -> F : A --> B )
2		ffn	|- ( F : A --> B -> F Fn A )
3	1 2	syl	|- ( ph -> F Fn A )