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 " A ) \ ( F " B ) ) C_ ( F " ( A \ B ) )

Proof

Step	Hyp	Ref	Expression
1		ssun2	|- A C_ ( B u. A )
2		undif2	|- ( B u. ( A \ B ) ) = ( B u. A )
3	1 2	sseqtrri	|- A C_ ( B u. ( A \ B ) )
4		imass2	|- ( A C_ ( B u. ( A \ B ) ) -> ( F " A ) C_ ( F " ( B u. ( A \ B ) ) ) )
5	3 4	ax-mp	|- ( F " A ) C_ ( F " ( B u. ( A \ B ) ) )
6		imaundi	|- ( F " ( B u. ( A \ B ) ) ) = ( ( F " B ) u. ( F " ( A \ B ) ) )
7	5 6	sseqtri	|- ( F " A ) C_ ( ( F " B ) u. ( F " ( A \ B ) ) )
8		ssundif	|- ( ( F " A ) C_ ( ( F " B ) u. ( F " ( A \ B ) ) ) <-> ( ( F " A ) \ ( F " B ) ) C_ ( F " ( A \ B ) ) )
9	7 8	mpbi	|- ( ( F " A ) \ ( F " B ) ) C_ ( F " ( A \ B ) )