Description: A function's value belongs to its range. (Contributed by NM, 15Oct1996)
Ref  Expression  

Assertion  fnfvelrn   ( ( F Fn A /\ B e. A ) > ( F ` B ) e. ran F ) 
Step  Hyp  Ref  Expression 

1  fvelrn   ( ( Fun F /\ B e. dom F ) > ( F ` B ) e. ran F ) 

2  1  funfni   ( ( F Fn A /\ B e. A ) > ( F ` B ) e. ran F ) 