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		fnrnfv	|- ( F Fn A -> ran F = { y | E. x e. A y = ( F ` x ) } )
2	1	unieqd	|- ( F Fn A -> U. ran F = U. { y | E. x e. A y = ( F ` x ) } )
3		fvex	|- ( F ` x ) e. _V
4	3	dfiun2	|- U_ x e. A ( F ` x ) = U. { y | E. x e. A y = ( F ` x ) }
5	2 4	syl6reqr	|- ( F Fn A -> U_ x e. A ( F ` x ) = U. ran F )