Theorem imass1

Description: Subset theorem for image. (Contributed by NM, 16-Mar-2004)

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

Proof

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