**Description:** The range of a function expressed as a collection of the function's
values. (Contributed by NM, 20-Oct-2005) (Proof shortened by Mario
Carneiro, 31-Aug-2015)

Ref | Expression | ||
---|---|---|---|

Assertion | fnrnfv | ⊢ ( 𝐹 Fn 𝐴 → ran 𝐹 = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) } ) |

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

1 | dffn5 | ⊢ ( 𝐹 Fn 𝐴 ↔ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) ) | |

2 | rneq | ⊢ ( 𝐹 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) → ran 𝐹 = ran ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) ) | |

3 | 1 2 | sylbi | ⊢ ( 𝐹 Fn 𝐴 → ran 𝐹 = ran ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) ) |

4 | eqid | ⊢ ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) | |

5 | 4 | rnmpt | ⊢ ran ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) } |

6 | 3 5 | syl6eq | ⊢ ( 𝐹 Fn 𝐴 → ran 𝐹 = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) } ) |