Theorem fniinfv

Description: The indexed intersection of a function's values is the intersection of its range. (Contributed by NM, 20-Oct-2005)

	Ref	Expression
Assertion	fniinfv	|- ( F Fn A -> |^|_ x e. A ( F ` x ) = |^| ran F )

Proof

Step	Hyp	Ref	Expression
1		fvex	|- ( F ` x ) e. _V
2	1	dfiin2	|- |^|_ x e. A ( F ` x ) = |^| { 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	inteqd	|- ( F Fn A -> |^| ran F = |^| { y | E. x e. A y = ( F ` x ) } )
5	2 4	eqtr4id	|- ( F Fn A -> |^|_ x e. A ( F ` x ) = |^| ran F )