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 -> U_ x e. A ( F ` x ) = U. ran F )

Proof

Step Hyp Ref Expression
1 fvex
 |-  ( F ` x ) e. _V
2 1 dfiun2
 |-  U_ x e. A ( F ` x ) = U. { y | E. x e. A y = ( F ` x ) }
3 fnrnfv
 |-  ( F Fn A -> ran F = { y | E. x e. A y = ( F ` x ) } )
4 3 unieqd
 |-  ( F Fn A -> U. ran F = U. { y | E. x e. A y = ( F ` x ) } )
5 2 4 eqtr4id
 |-  ( F Fn A -> U_ x e. A ( F ` x ) = U. ran F )