Theorem funforn

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

	Ref	Expression
Assertion	funforn	⊢ ( Fun 𝐴 ↔ 𝐴 : dom 𝐴 –onto→ ran 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		funfn	⊢ ( Fun 𝐴 ↔ 𝐴 Fn dom 𝐴 )
2		dffn4	⊢ ( 𝐴 Fn dom 𝐴 ↔ 𝐴 : dom 𝐴 –onto→ ran 𝐴 )
3	1 2	bitri	⊢ ( Fun 𝐴 ↔ 𝐴 : dom 𝐴 –onto→ ran 𝐴 )