Theorem foima

Description: The image of the domain of an onto function. (Contributed by NM, 29-Nov-2002)

	Ref	Expression
Assertion	foima	$$⊢F:A\underset{onto}{⟶}B\to F\left[A\right]=B$$

Proof

Step	Hyp	Ref	Expression
1		imadmrn	$$⊢F\left[\mathrm{dom}F\right]=\mathrm{ran}F$$
2		fof	$$⊢F:A\underset{onto}{⟶}B\to F:A⟶B$$
3	2	fdmd	$$⊢F:A\underset{onto}{⟶}B\to \mathrm{dom}F=A$$
4	3	imaeq2d	$$⊢F:A\underset{onto}{⟶}B\to F\left[\mathrm{dom}F\right]=F\left[A\right]$$
5		forn	$$⊢F:A\underset{onto}{⟶}B\to \mathrm{ran}F=B$$
6	1 4 5	3eqtr3a	$$⊢F:A\underset{onto}{⟶}B\to F\left[A\right]=B$$