Theorem difpreima

Description: Preimage of a difference. (Contributed by Mario Carneiro, 14-Jun-2016)

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

Proof

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