Theorem f1ofo

Description: A one-to-one onto function is an onto function. (Contributed by NM, 28-Apr-2004)

	Ref	Expression
Assertion	f1ofo	$$⊢F:A\underset{1-1\; onto}{⟶}B\to F:A\underset{onto}{⟶}B$$

Proof

Step	Hyp	Ref	Expression
1		dff1o3	$$⊢F:A\underset{1-1\; onto}{⟶}B\leftrightarrow \left(F:A\underset{onto}{⟶}B\wedge \mathrm{Fun}{F}^{-1}\right)$$
2	1	simplbi	$$⊢F:A\underset{1-1\; onto}{⟶}B\to F:A\underset{onto}{⟶}B$$