Metamath Proof Explorer


Theorem fniunfv

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 𝐹 )

Proof

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 𝐹 )