Metamath Proof Explorer

Theorem fnima

Description: The image of a function's domain is its range. (Contributed by NM, 4-Nov-2004) (Proof shortened by Andrew Salmon, 17-Sep-2011)

Ref Expression
Assertion fnima 
|- ( F Fn A -> ( F " A ) = ran F )

Proof

Step Hyp Ref Expression
1 df-ima 
 |-  ( F " A ) = ran ( F |` A )
2 fnresdm 
 |-  ( F Fn A -> ( F |` A ) = F )
3 2 rneqd 
 |-  ( F Fn A -> ran ( F |` A ) = ran F )
4 1 3 eqtrid 
 |-  ( F Fn A -> ( F " A ) = ran F )