Theorem fof

Description: An onto mapping is a mapping. (Contributed by NM, 3-Aug-1994)

	Ref	Expression
Assertion	fof	$$⊢F:A\underset{onto}{⟶}B\to F:A⟶B$$

Proof

Step	Hyp	Ref	Expression
1		eqimss	$$⊢\mathrm{ran}F=B\to \mathrm{ran}F\subseteq B$$
2	1	anim2i	$$⊢\left(FFnA\wedge \mathrm{ran}F=B\right)\to \left(FFnA\wedge \mathrm{ran}F\subseteq B\right)$$
3		df-fo	$$⊢F:A\underset{onto}{⟶}B\leftrightarrow \left(FFnA\wedge \mathrm{ran}F=B\right)$$
4		df-f	$$⊢F:A⟶B\leftrightarrow \left(FFnA\wedge \mathrm{ran}F\subseteq B\right)$$
5	2 3 4	3imtr4i	$$⊢F:A\underset{onto}{⟶}B\to F:A⟶B$$