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 5875 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ↾ 𝐴) ⊆ (𝐶 ↾ 𝐵)) | |
2 | rnss 5803 | . . 3 ⊢ ((𝐶 ↾ 𝐴) ⊆ (𝐶 ↾ 𝐵) → ran (𝐶 ↾ 𝐴) ⊆ ran (𝐶 ↾ 𝐵)) | |
3 | 1, 2 | syl 17 | . 2 ⊢ (𝐴 ⊆ 𝐵 → ran (𝐶 ↾ 𝐴) ⊆ ran (𝐶 ↾ 𝐵)) |
4 | df-ima 5562 | . 2 ⊢ (𝐶 “ 𝐴) = ran (𝐶 ↾ 𝐴) | |
5 | df-ima 5562 | . 2 ⊢ (𝐶 “ 𝐵) = ran (𝐶 ↾ 𝐵) | |
6 | 3, 4, 5 | 3sstr4g 4011 | 1 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 “ 𝐴) ⊆ (𝐶 “ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ⊆ wss 3935 ran crn 5550 ↾ cres 5551 “ cima 5552 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2793 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-rab 3147 df-v 3497 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-nul 4291 df-if 4466 df-sn 4560 df-pr 4562 df-op 4566 df-br 5059 df-opab 5121 df-xp 5555 df-cnv 5557 df-dm 5559 df-rn 5560 df-res 5561 df-ima 5562 |
This theorem is referenced by: funimass1 6430 funimass2 6431 fvimacnv 6816 fnfvimad 6987 f1imass 7013 ecinxp 8362 sbthlem1 8616 sbthlem2 8617 php3 8692 ordtypelem2 8972 tcrank 9302 limsupgord 14819 isercoll 15014 isacs1i 16918 gsumzf1o 18963 dprdres 19081 dprd2da 19095 dmdprdsplit2lem 19098 lmhmlsp 19752 f1lindf 20896 iscnp4 21801 cnpco 21805 cncls2i 21808 cnntri 21809 cnrest2 21824 cnpresti 21826 cnprest 21827 1stcfb 21983 xkococnlem 22197 qtopval2 22234 tgqtop 22250 qtoprest 22255 kqdisj 22270 regr1lem 22277 kqreglem1 22279 kqreglem2 22280 kqnrmlem1 22281 kqnrmlem2 22282 nrmhmph 22332 fbasrn 22422 elfm2 22486 fmfnfmlem1 22492 fmco 22499 flffbas 22533 cnpflf2 22538 cnextcn 22605 metcnp3 23079 metustto 23092 cfilucfil 23098 uniioombllem3 24115 dyadmbllem 24129 mbfconstlem 24157 i1fima2 24209 itg2gt0 24290 ellimc3 24406 limcflf 24408 limcresi 24412 limciun 24421 lhop 24542 ig1peu 24694 ig1pdvds 24699 psercnlem2 24941 dvloglem 25158 efopn 25168 fnpreimac 30345 txomap 30998 tpr2rico 31055 pthhashvtx 32272 cvmsss2 32419 cvmopnlem 32423 cvmliftmolem1 32426 cvmliftlem15 32443 cvmlift2lem9 32456 imadifss 34749 poimirlem1 34775 poimirlem2 34776 poimirlem3 34777 poimirlem15 34789 poimirlem30 34804 dvtan 34824 heibor1lem 34970 isnumbasabl 39586 isnumbasgrp 39587 dfacbasgrp 39588 trclimalb2 39951 frege81d 39972 imass2d 41416 limccog 41781 liminfgord 41915 |
Copyright terms: Public domain | W3C validator |