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 )