Theorem fnima

Description: The image of a function's domain is its range. (Contributed by NM, 4-Nov-2004) (Proof shortened by Andrew Salmon, 17-Sep-2011)

	Ref	Expression
Assertion	fnima	$$⊢FFnA\to F\left[A\right]=\mathrm{ran}F$$

Proof

Step	Hyp	Ref	Expression
1		df-ima	$$⊢F\left[A\right]=\mathrm{ran}\left({F\upharpoonright }_A\right)$$
2		fnresdm	$$⊢FFnA\to {F\upharpoonright }_A=F$$
3	2	rneqd	$$⊢FFnA\to \mathrm{ran}\left({F\upharpoonright }_A\right)=\mathrm{ran}F$$
4	1 3	syl5eq	$$⊢FFnA\to F\left[A\right]=\mathrm{ran}F$$