![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > imass2 | Structured version Visualization version GIF version |
Description: Subset theorem for image. Exercise 22(a) of [Enderton] p. 53. (Contributed by NM, 22-Mar-1998.) |
Ref | Expression |
---|---|
imass2 | ⊢ (𝐴 ⊆ 𝐵 → (𝐶 “ 𝐴) ⊆ (𝐶 “ 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssres2 6024 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ↾ 𝐴) ⊆ (𝐶 ↾ 𝐵)) | |
2 | rnss 5952 | . . 3 ⊢ ((𝐶 ↾ 𝐴) ⊆ (𝐶 ↾ 𝐵) → ran (𝐶 ↾ 𝐴) ⊆ ran (𝐶 ↾ 𝐵)) | |
3 | 1, 2 | syl 17 | . 2 ⊢ (𝐴 ⊆ 𝐵 → ran (𝐶 ↾ 𝐴) ⊆ ran (𝐶 ↾ 𝐵)) |
4 | df-ima 5701 | . 2 ⊢ (𝐶 “ 𝐴) = ran (𝐶 ↾ 𝐴) | |
5 | df-ima 5701 | . 2 ⊢ (𝐶 “ 𝐵) = ran (𝐶 ↾ 𝐵) | |
6 | 3, 4, 5 | 3sstr4g 4040 | 1 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 “ 𝐴) ⊆ (𝐶 “ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ⊆ wss 3962 ran crn 5689 ↾ cres 5690 “ cima 5691 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-8 2107 ax-9 2115 ax-ext 2705 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1539 df-fal 1549 df-ex 1776 df-sb 2062 df-clab 2712 df-cleq 2726 df-clel 2813 df-rab 3433 df-v 3479 df-dif 3965 df-un 3967 df-in 3969 df-ss 3979 df-nul 4339 df-if 4531 df-sn 4631 df-pr 4633 df-op 4637 df-br 5148 df-opab 5210 df-xp 5694 df-cnv 5696 df-dm 5698 df-rn 5699 df-res 5700 df-ima 5701 |
This theorem is referenced by: funimass1 6649 funimass2 6650 fvimacnv 7072 fnfvimad 7253 f1imass 7283 ecinxp 8830 sbthlem1 9121 sbthlem2 9122 php3 9246 php3OLD 9258 ordtypelem2 9556 tcrank 9921 limsupgord 15504 isercoll 15700 isacs1i 17701 gsumzf1o 19944 dprdres 20062 dprd2da 20076 dmdprdsplit2lem 20079 lmhmlsp 21065 f1lindf 21859 iscnp4 23286 cnpco 23290 cncls2i 23293 cnntri 23294 cnrest2 23309 cnpresti 23311 cnprest 23312 1stcfb 23468 xkococnlem 23682 qtopval2 23719 tgqtop 23735 qtoprest 23740 kqdisj 23755 regr1lem 23762 kqreglem1 23764 kqreglem2 23765 kqnrmlem1 23766 kqnrmlem2 23767 nrmhmph 23817 fbasrn 23907 elfm2 23971 fmfnfmlem1 23977 fmco 23984 flffbas 24018 cnpflf2 24023 cnextcn 24090 metcnp3 24568 metustto 24581 cfilucfil 24587 uniioombllem3 25633 dyadmbllem 25647 mbfconstlem 25675 i1fima2 25727 itg2gt0 25809 ellimc3 25928 limcflf 25930 limcresi 25934 limciun 25943 lhop 26069 ig1peu 26228 ig1pdvds 26233 psercnlem2 26482 dvloglem 26704 efopn 26714 noetalem1 27800 madess 27929 cofcut1 27968 negsproplem2 28075 fnpreimac 32687 fsuppinisegfi 32701 gsumpart 33042 txomap 33794 zarcmplem 33841 tpr2rico 33872 pthhashvtx 35111 cvmsss2 35258 cvmopnlem 35262 cvmliftmolem1 35265 cvmliftlem15 35282 cvmlift2lem9 35295 imadifss 37581 poimirlem1 37607 poimirlem2 37608 poimirlem3 37609 poimirlem15 37621 poimirlem30 37636 dvtan 37656 heibor1lem 37795 aks6d1c2 42111 aks6d1c6lem3 42153 aks6d1c6lem5 42158 isnumbasabl 43094 isnumbasgrp 43095 dfacbasgrp 43096 trclimalb2 43715 frege81d 43736 imass2d 45206 limccog 45575 liminfgord 45709 uhgrimisgrgriclem 47835 clnbgrgrim 47839 |
Copyright terms: Public domain | W3C validator |