Metamath Proof Explorer


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 𝐴 )