Metamath Proof Explorer

Theorem imass2d

Description: Subset theorem for image. (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Hypothesis imass2d.1 
|- ( ph -> A C_ B )
Assertion imass2d 
|- ( ph -> ( C " A ) C_ ( C " B ) )

Proof

Step Hyp Ref Expression
1 imass2d.1 
 |-  ( ph -> A C_ B )
2 imass2 
 |-  ( A C_ B -> ( C " A ) C_ ( C " B ) )
3 1 2 syl 
 |-  ( ph -> ( C " A ) C_ ( C " B ) )