Theorem inpreima

Description: Preimage of an intersection. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 14-Jun-2016)

	Ref	Expression
Assertion	inpreima	$$⊢\mathrm{Fun}F\to F^{-1}\left[A\cap B\right]=F^{-1}\left[A\right]\cap F^{-1}\left[B\right]$$

Proof

Step	Hyp	Ref	Expression
1		funcnvcnv	$$⊢\mathrm{Fun}F\to \mathrm{Fun}{F^{-1}}^{-1}$$
2		imain	$$⊢\mathrm{Fun}{F^{-1}}^{-1}\to F^{-1}\left[A\cap B\right]=F^{-1}\left[A\right]\cap F^{-1}\left[B\right]$$
3	1 2	syl	$$⊢\mathrm{Fun}F\to F^{-1}\left[A\cap B\right]=F^{-1}\left[A\right]\cap F^{-1}\left[B\right]$$