Metamath Proof Explorer


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 ) )