**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 | ⊢ ( 𝐹 Fn 𝐴 → ( 𝐹 “ 𝐴 ) = ran 𝐹 ) |

Step | Hyp | Ref | Expression |
---|---|---|---|

1 | df-ima | ⊢ ( 𝐹 “ 𝐴 ) = ran ( 𝐹 ↾ 𝐴 ) | |

2 | fnresdm | ⊢ ( 𝐹 Fn 𝐴 → ( 𝐹 ↾ 𝐴 ) = 𝐹 ) | |

3 | 2 | rneqd | ⊢ ( 𝐹 Fn 𝐴 → ran ( 𝐹 ↾ 𝐴 ) = ran 𝐹 ) |

4 | 1 3 | syl5eq | ⊢ ( 𝐹 Fn 𝐴 → ( 𝐹 “ 𝐴 ) = ran 𝐹 ) |