Theorem f1orn

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

	Ref	Expression
Assertion	f1orn	⊢ ( 𝐹 : 𝐴 –1-1-onto→ ran 𝐹 ↔ ( 𝐹 Fn 𝐴 ∧ Fun ◡ 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		dff1o2	⊢ ( 𝐹 : 𝐴 –1-1-onto→ ran 𝐹 ↔ ( 𝐹 Fn 𝐴 ∧ Fun ◡ 𝐹 ∧ ran 𝐹 = ran 𝐹 ) )
2		eqid	⊢ ran 𝐹 = ran 𝐹
3		df-3an	⊢ ( ( 𝐹 Fn 𝐴 ∧ Fun ◡ 𝐹 ∧ ran 𝐹 = ran 𝐹 ) ↔ ( ( 𝐹 Fn 𝐴 ∧ Fun ◡ 𝐹 ) ∧ ran 𝐹 = ran 𝐹 ) )
4	2 3	mpbiran2	⊢ ( ( 𝐹 Fn 𝐴 ∧ Fun ◡ 𝐹 ∧ ran 𝐹 = ran 𝐹 ) ↔ ( 𝐹 Fn 𝐴 ∧ Fun ◡ 𝐹 ) )
5	1 4	bitri	⊢ ( 𝐹 : 𝐴 –1-1-onto→ ran 𝐹 ↔ ( 𝐹 Fn 𝐴 ∧ Fun ◡ 𝐹 ) )