Theorem ffrn

Description: A function maps to its range. (Contributed by Glauco Siliprandi, 3-Mar-2021)

	Ref	Expression
Assertion	ffrn	$$⊢F:A⟶B\to F:A⟶\mathrm{ran}F$$

Proof

Step	Hyp	Ref	Expression
1		ffn	$$⊢F:A⟶B\to FFnA$$
2		dffn3	$$⊢FFnA\leftrightarrow F:A⟶\mathrm{ran}F$$
3	1 2	sylib	$$⊢F:A⟶B\to F:A⟶\mathrm{ran}F$$