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 F Fn A x A F x = ran F

Proof

Step Hyp Ref Expression
1 fnrnfv F Fn A ran F = y | x A y = F x
2 1 unieqd F Fn A ran F = y | x A y = F x
3 fvex F x V
4 3 dfiun2 x A F x = y | x A y = F x
5 2 4 syl6reqr F Fn A x A F x = ran F