Theorem intpreima

Description: Preimage of an intersection. (Contributed by FL, 28-Apr-2012)

	Ref	Expression
Assertion	intpreima	$$⊢\left(\mathrm{Fun}F\wedge A\ne \varnothing \right)\to F^{-1}\left[\bigcap A\right]=\bigcap _{x\in A}{F}^{-1}\left[x\right]$$

Proof

Step	Hyp	Ref	Expression
1		intiin	$$⊢\bigcap A=\bigcap _{x\in A}x$$
2	1	imaeq2i	$$⊢F^{-1}\left[\bigcap A\right]=F^{-1}\left[\bigcap _{x\in A}x\right]$$
3		iinpreima	$$⊢\left(\mathrm{Fun}F\wedge A\ne \varnothing \right)\to F^{-1}\left[\bigcap _{x\in A}x\right]=\bigcap _{x\in A}{F}^{-1}\left[x\right]$$
4	2 3	syl5eq	$$⊢\left(\mathrm{Fun}F\wedge A\ne \varnothing \right)\to F^{-1}\left[\bigcap A\right]=\bigcap _{x\in A}{F}^{-1}\left[x\right]$$