![]() |
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 5674 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ↾ 𝐴) ⊆ (𝐶 ↾ 𝐵)) | |
2 | rnss 5599 | . . 3 ⊢ ((𝐶 ↾ 𝐴) ⊆ (𝐶 ↾ 𝐵) → ran (𝐶 ↾ 𝐴) ⊆ ran (𝐶 ↾ 𝐵)) | |
3 | 1, 2 | syl 17 | . 2 ⊢ (𝐴 ⊆ 𝐵 → ran (𝐶 ↾ 𝐴) ⊆ ran (𝐶 ↾ 𝐵)) |
4 | df-ima 5368 | . 2 ⊢ (𝐶 “ 𝐴) = ran (𝐶 ↾ 𝐴) | |
5 | df-ima 5368 | . 2 ⊢ (𝐶 “ 𝐵) = ran (𝐶 ↾ 𝐵) | |
6 | 3, 4, 5 | 3sstr4g 3865 | 1 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 “ 𝐴) ⊆ (𝐶 “ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ⊆ wss 3792 ran crn 5356 ↾ cres 5357 “ cima 5358 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-13 2334 ax-ext 2754 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-3an 1073 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-rab 3099 df-v 3400 df-dif 3795 df-un 3797 df-in 3799 df-ss 3806 df-nul 4142 df-if 4308 df-sn 4399 df-pr 4401 df-op 4405 df-br 4887 df-opab 4949 df-xp 5361 df-cnv 5363 df-dm 5365 df-rn 5366 df-res 5367 df-ima 5368 |
This theorem is referenced by: funimass1 6216 funimass2 6217 fvimacnv 6595 fnfvimad 6766 f1imass 6793 ecinxp 8105 sbthlem1 8358 sbthlem2 8359 php3 8434 ordtypelem2 8713 tcrank 9044 limsupgord 14611 isercoll 14806 isacs1i 16703 gsumzf1o 18699 dprdres 18814 dprd2da 18828 dmdprdsplit2lem 18831 lmhmlsp 19444 f1lindf 20565 iscnp4 21475 cnpco 21479 cncls2i 21482 cnntri 21483 cnrest2 21498 cnpresti 21500 cnprest 21501 1stcfb 21657 xkococnlem 21871 qtopval2 21908 tgqtop 21924 qtoprest 21929 kqdisj 21944 regr1lem 21951 kqreglem1 21953 kqreglem2 21954 kqnrmlem1 21955 kqnrmlem2 21956 nrmhmph 22006 fbasrn 22096 elfm2 22160 fmfnfmlem1 22166 fmco 22173 flffbas 22207 cnpflf2 22212 cnextcn 22279 metcnp3 22753 metustto 22766 cfilucfil 22772 uniioombllem3 23789 dyadmbllem 23803 mbfconstlem 23831 i1fima2 23883 itg2gt0 23964 ellimc3 24080 limcflf 24082 limcresi 24086 limciun 24095 lhop 24216 ig1peu 24368 ig1pdvds 24373 psercnlem2 24615 dvloglem 24831 efopn 24841 fnpreimac 30036 txomap 30499 tpr2rico 30556 cvmsss2 31855 cvmopnlem 31859 cvmliftmolem1 31862 cvmliftlem15 31879 cvmlift2lem9 31892 imadifss 34011 poimirlem1 34038 poimirlem2 34039 poimirlem3 34040 poimirlem15 34052 poimirlem30 34067 dvtan 34087 heibor1lem 34234 isnumbasabl 38639 isnumbasgrp 38640 dfacbasgrp 38641 trclimalb2 38979 frege81d 39000 fnfvima2 40393 imass2d 40395 limccog 40764 liminfgord 40898 |
Copyright terms: Public domain | W3C validator |