**Description:** Subset theorem for image. Exercise 22(a) of Enderton p. 53.
(Contributed by NM, 22-Mar-1998)

Ref | Expression | ||
---|---|---|---|

Assertion | imass2 | ⊢ ( 𝐴 ⊆ 𝐵 → ( 𝐶 “ 𝐴 ) ⊆ ( 𝐶 “ 𝐵 ) ) |

Step | Hyp | Ref | Expression |
---|---|---|---|

1 | ssres2 | ⊢ ( 𝐴 ⊆ 𝐵 → ( 𝐶 ↾ 𝐴 ) ⊆ ( 𝐶 ↾ 𝐵 ) ) | |

2 | rnss | ⊢ ( ( 𝐶 ↾ 𝐴 ) ⊆ ( 𝐶 ↾ 𝐵 ) → ran ( 𝐶 ↾ 𝐴 ) ⊆ ran ( 𝐶 ↾ 𝐵 ) ) | |

3 | 1 2 | syl | ⊢ ( 𝐴 ⊆ 𝐵 → ran ( 𝐶 ↾ 𝐴 ) ⊆ ran ( 𝐶 ↾ 𝐵 ) ) |

4 | df-ima | ⊢ ( 𝐶 “ 𝐴 ) = ran ( 𝐶 ↾ 𝐴 ) | |

5 | df-ima | ⊢ ( 𝐶 “ 𝐵 ) = ran ( 𝐶 ↾ 𝐵 ) | |

6 | 3 4 5 | 3sstr4g | ⊢ ( 𝐴 ⊆ 𝐵 → ( 𝐶 “ 𝐴 ) ⊆ ( 𝐶 “ 𝐵 ) ) |