Theorem f1orn

Description: A one-to-one function maps onto its range. (Contributed by NM, 13-Aug-2004)

	Ref	Expression
Assertion	f1orn	|- ( F : A -1-1-onto-> ran F <-> ( F Fn A /\ Fun `' F ) )

Proof

Step	Hyp	Ref	Expression
1		dff1o2	|- ( F : A -1-1-onto-> ran F <-> ( F Fn A /\ Fun `' F /\ ran F = ran F ) )
2		eqid	|- ran F = ran F
3		df-3an	|- ( ( F Fn A /\ Fun `' F /\ ran F = ran F ) <-> ( ( F Fn A /\ Fun `' F ) /\ ran F = ran F ) )
4	2 3	mpbiran2	|- ( ( F Fn A /\ Fun `' F /\ ran F = ran F ) <-> ( F Fn A /\ Fun `' F ) )
5	1 4	bitri	|- ( F : A -1-1-onto-> ran F <-> ( F Fn A /\ Fun `' F ) )