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 fvex F x V
2 1 dfiun2 x A F x = y | x A y = F x
3 fnrnfv F Fn A ran F = y | x A y = F x
4 3 unieqd F Fn A ran F = y | x A y = F x
5 2 4 eqtr4id F Fn A x A F x = ran F