Metamath Proof Explorer

Theorem dffn4

Description: A function maps onto its range. (Contributed by NM, 10-May-1998)

Ref Expression
Assertion dffn4 
|- ( F Fn A <-> F : A -onto-> ran F )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ran F = ran F
2 1 biantru 
 |-  ( F Fn A <-> ( F Fn A /\ ran F = ran F ) )
3 df-fo 
 |-  ( F : A -onto-> ran F <-> ( F Fn A /\ ran F = ran F ) )
4 2 3 bitr4i 
 |-  ( F Fn A <-> F : A -onto-> ran F )