Theorem funforn

Description: A function maps its domain onto its range. (Contributed by NM, 23-Jul-2004)

	Ref	Expression
Assertion	funforn	$$⊢\mathrm{Fun}A\leftrightarrow A:\mathrm{dom}A\underset{onto}{⟶}\mathrm{ran}A$$

Proof

Step	Hyp	Ref	Expression
1		funfn	$$⊢\mathrm{Fun}A\leftrightarrow AFn\mathrm{dom}A$$
2		dffn4	$$⊢AFn\mathrm{dom}A\leftrightarrow A:\mathrm{dom}A\underset{onto}{⟶}\mathrm{ran}A$$
3	1 2	bitri	$$⊢\mathrm{Fun}A\leftrightarrow A:\mathrm{dom}A\underset{onto}{⟶}\mathrm{ran}A$$