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	$$⊢FFnA\to \bigcap _{x\in A}F\left(x\right)=\bigcap \mathrm{ran}F$$

Proof

Step	Hyp	Ref	Expression
1		fvex	$$⊢F\left(x\right)\in \mathrm{V}$$
2	1	dfiin2	$$⊢\bigcap _{x\in A}F\left(x\right)=\bigcap \left\{y|\exists x\in Ay=F\left(x\right)\right\}$$
3		fnrnfv	$$⊢FFnA\to \mathrm{ran}F=\left\{y|\exists x\in Ay=F\left(x\right)\right\}$$
4	3	inteqd	$$⊢FFnA\to \bigcap \mathrm{ran}F=\bigcap \left\{y|\exists x\in Ay=F\left(x\right)\right\}$$
5	2 4	eqtr4id	$$⊢FFnA\to \bigcap _{x\in A}F\left(x\right)=\bigcap \mathrm{ran}F$$