Description: The range of a mapping. (Contributed by NM, 3Aug1994)
Ref  Expression  

Assertion  frn   ( F : A > B > ran F C_ B ) 
Step  Hyp  Ref  Expression 

1  dff   ( F : A > B <> ( F Fn A /\ ran F C_ B ) ) 

2  1  simprbi   ( F : A > B > ran F C_ B ) 