Metamath Proof Explorer

Theorem forn

Description: The codomain of an onto function is its range. (Contributed by NM, 3-Aug-1994)

Ref Expression
Assertion forn 
|- ( F : A -onto-> B -> ran F = B )

Proof

Step Hyp Ref Expression
1 df-fo 
 |-  ( F : A -onto-> B <-> ( F Fn A /\ ran F = B ) )
2 1 simprbi 
 |-  ( F : A -onto-> B -> ran F = B )