![]() |
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 6010 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ↾ 𝐴) ⊆ (𝐶 ↾ 𝐵)) | |
2 | rnss 5939 | . . 3 ⊢ ((𝐶 ↾ 𝐴) ⊆ (𝐶 ↾ 𝐵) → ran (𝐶 ↾ 𝐴) ⊆ ran (𝐶 ↾ 𝐵)) | |
3 | 1, 2 | syl 17 | . 2 ⊢ (𝐴 ⊆ 𝐵 → ran (𝐶 ↾ 𝐴) ⊆ ran (𝐶 ↾ 𝐵)) |
4 | df-ima 5690 | . 2 ⊢ (𝐶 “ 𝐴) = ran (𝐶 ↾ 𝐴) | |
5 | df-ima 5690 | . 2 ⊢ (𝐶 “ 𝐵) = ran (𝐶 ↾ 𝐵) | |
6 | 3, 4, 5 | 3sstr4g 4028 | 1 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 “ 𝐴) ⊆ (𝐶 “ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ⊆ wss 3949 ran crn 5678 ↾ cres 5679 “ cima 5680 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-rab 3434 df-v 3477 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-nul 4324 df-if 4530 df-sn 4630 df-pr 4632 df-op 4636 df-br 5150 df-opab 5212 df-xp 5683 df-cnv 5685 df-dm 5687 df-rn 5688 df-res 5689 df-ima 5690 |
This theorem is referenced by: funimass1 6631 funimass2 6632 fvimacnv 7055 fnfvimad 7236 f1imass 7263 ecinxp 8786 sbthlem1 9083 sbthlem2 9084 php3 9212 php3OLD 9224 ordtypelem2 9514 tcrank 9879 limsupgord 15416 isercoll 15614 isacs1i 17601 gsumzf1o 19780 dprdres 19898 dprd2da 19912 dmdprdsplit2lem 19915 lmhmlsp 20660 f1lindf 21377 iscnp4 22767 cnpco 22771 cncls2i 22774 cnntri 22775 cnrest2 22790 cnpresti 22792 cnprest 22793 1stcfb 22949 xkococnlem 23163 qtopval2 23200 tgqtop 23216 qtoprest 23221 kqdisj 23236 regr1lem 23243 kqreglem1 23245 kqreglem2 23246 kqnrmlem1 23247 kqnrmlem2 23248 nrmhmph 23298 fbasrn 23388 elfm2 23452 fmfnfmlem1 23458 fmco 23465 flffbas 23499 cnpflf2 23504 cnextcn 23571 metcnp3 24049 metustto 24062 cfilucfil 24068 uniioombllem3 25102 dyadmbllem 25116 mbfconstlem 25144 i1fima2 25196 itg2gt0 25278 ellimc3 25396 limcflf 25398 limcresi 25402 limciun 25411 lhop 25533 ig1peu 25689 ig1pdvds 25694 psercnlem2 25936 dvloglem 26156 efopn 26166 noetalem1 27244 madess 27371 cofcut1 27407 negsproplem2 27503 fnpreimac 31896 fsuppinisegfi 31909 gsumpart 32207 txomap 32814 zarcmplem 32861 tpr2rico 32892 pthhashvtx 34118 cvmsss2 34265 cvmopnlem 34269 cvmliftmolem1 34272 cvmliftlem15 34289 cvmlift2lem9 34302 imadifss 36463 poimirlem1 36489 poimirlem2 36490 poimirlem3 36491 poimirlem15 36503 poimirlem30 36518 dvtan 36538 heibor1lem 36677 isnumbasabl 41848 isnumbasgrp 41849 dfacbasgrp 41850 trclimalb2 42477 frege81d 42498 imass2d 43966 limccog 44336 liminfgord 44470 |
Copyright terms: Public domain | W3C validator |