Theorem ffnd

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

	Ref	Expression
Hypothesis	ffnd.1	$$⊢\phi \to F:A⟶B$$
Assertion	ffnd	$$⊢\phi \to FFnA$$

Proof

Step	Hyp	Ref	Expression
1		ffnd.1	$$⊢\phi \to F:A⟶B$$
2		ffn	$$⊢F:A⟶B\to FFnA$$
3	1 2	syl	$$⊢\phi \to FFnA$$