Metamath Proof Explorer

Theorem resimass

Description: The image of a restriction is a subset of the original image. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Assertion resimass 
|- ( ( A |` B ) " C ) C_ ( A " C )

Proof

Step Hyp Ref Expression
1 resss 
 |-  ( A |` B ) C_ A
2 imass1 
 |-  ( ( A |` B ) C_ A -> ( ( A |` B ) " C ) C_ ( A " C ) )
3 1 2 ax-mp 
 |-  ( ( A |` B ) " C ) C_ ( A " C )