**Description:** The indexed union of a function's values is the union of its range.
Compare Definition 5.4 of Monk1 p. 50. (Contributed by NM, 27-Sep-2004)

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

Assertion | fniunfv | ⊢ ( 𝐹 Fn 𝐴 → ∪ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ∪ ran 𝐹 ) |

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

1 | fvex | ⊢ ( 𝐹 ‘ 𝑥 ) ∈ V | |

2 | 1 | dfiun2 | ⊢ ∪ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ∪ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) } |

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

4 | 3 | unieqd | ⊢ ( 𝐹 Fn 𝐴 → ∪ ran 𝐹 = ∪ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) } ) |

5 | 2 4 | eqtr4id | ⊢ ( 𝐹 Fn 𝐴 → ∪ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ∪ ran 𝐹 ) |