Theorem imass2

Description: Subset theorem for image. Exercise 22(a) of Enderton p. 53. (Contributed by NM, 22-Mar-1998)

	Ref	Expression
Assertion	imass2	|- ( A C_ B -> ( C " A ) C_ ( C " B ) )

Proof

Step	Hyp	Ref	Expression
1		ssres2	|- ( A C_ B -> ( C |` A ) C_ ( C |` B ) )
2		rnss	|- ( ( C |` A ) C_ ( C |` B ) -> ran ( C |` A ) C_ ran ( C |` B ) )
3	1 2	syl	|- ( A C_ B -> ran ( C |` A ) C_ ran ( C |` B ) )
4		df-ima	|- ( C " A ) = ran ( C |` A )
5		df-ima	|- ( C " B ) = ran ( C |` B )
6	3 4 5	3sstr4g	|- ( A C_ B -> ( C " A ) C_ ( C " B ) )