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 ( ( 𝐴𝐵 ) “ 𝐶 ) ⊆ ( 𝐴𝐶 )

Proof

Step Hyp Ref Expression
1 resss ( 𝐴𝐵 ) ⊆ 𝐴
2 imass1 ( ( 𝐴𝐵 ) ⊆ 𝐴 → ( ( 𝐴𝐵 ) “ 𝐶 ) ⊆ ( 𝐴𝐶 ) )
3 1 2 ax-mp ( ( 𝐴𝐵 ) “ 𝐶 ) ⊆ ( 𝐴𝐶 )