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 A <-> A : dom A -onto-> ran A )

Proof

Step Hyp Ref Expression
1 funfn 
 |-  ( Fun A <-> A Fn dom A )
2 dffn4 
 |-  ( A Fn dom A <-> A : dom A -onto-> ran A )
3 1 2 bitri 
 |-  ( Fun A <-> A : dom A -onto-> ran A )