Theorem imadifss

Description: The difference of images is a subset of the image of the difference. (Contributed by Brendan Leahy, 21-Aug-2020)

	Ref	Expression
Assertion	imadifss	$$⊢F\left[A\right]\setminus F\left[B\right]\subseteq F\left[A\setminus B\right]$$

Proof

Step	Hyp	Ref	Expression
1		ssun2	$$⊢A\subseteq B\cup A$$
2		undif2	$$⊢B\cup \left(A\setminus B\right)=B\cup A$$
3	1 2	sseqtrri	$$⊢A\subseteq B\cup \left(A\setminus B\right)$$
4		imass2	$$⊢A\subseteq B\cup \left(A\setminus B\right)\to F\left[A\right]\subseteq F\left[B\cup \left(A\setminus B\right)\right]$$
5	3 4	ax-mp	$$⊢F\left[A\right]\subseteq F\left[B\cup \left(A\setminus B\right)\right]$$
6		imaundi	$$⊢F\left[B\cup \left(A\setminus B\right)\right]=F\left[B\right]\cup F\left[A\setminus B\right]$$
7	5 6	sseqtri	$$⊢F\left[A\right]\subseteq F\left[B\right]\cup F\left[A\setminus B\right]$$
8		ssundif	$$⊢F\left[A\right]\subseteq F\left[B\right]\cup F\left[A\setminus B\right]\leftrightarrow F\left[A\right]\setminus F\left[B\right]\subseteq F\left[A\setminus B\right]$$
9	7 8	mpbi	$$⊢F\left[A\right]\setminus F\left[B\right]\subseteq F\left[A\setminus B\right]$$