![]() |
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 6014 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ↾ 𝐴) ⊆ (𝐶 ↾ 𝐵)) | |
2 | rnss 5945 | . . 3 ⊢ ((𝐶 ↾ 𝐴) ⊆ (𝐶 ↾ 𝐵) → ran (𝐶 ↾ 𝐴) ⊆ ran (𝐶 ↾ 𝐵)) | |
3 | 1, 2 | syl 17 | . 2 ⊢ (𝐴 ⊆ 𝐵 → ran (𝐶 ↾ 𝐴) ⊆ ran (𝐶 ↾ 𝐵)) |
4 | df-ima 5695 | . 2 ⊢ (𝐶 “ 𝐴) = ran (𝐶 ↾ 𝐴) | |
5 | df-ima 5695 | . 2 ⊢ (𝐶 “ 𝐵) = ran (𝐶 ↾ 𝐵) | |
6 | 3, 4, 5 | 3sstr4g 4025 | 1 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 “ 𝐴) ⊆ (𝐶 “ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ⊆ wss 3947 ran crn 5683 ↾ cres 5684 “ cima 5685 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1537 df-fal 1547 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-rab 3420 df-v 3464 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4326 df-if 4534 df-sn 4634 df-pr 4636 df-op 4640 df-br 5154 df-opab 5216 df-xp 5688 df-cnv 5690 df-dm 5692 df-rn 5693 df-res 5694 df-ima 5695 |
This theorem is referenced by: funimass1 6641 funimass2 6642 fvimacnv 7066 fnfvimad 7251 f1imass 7279 ecinxp 8821 sbthlem1 9121 sbthlem2 9122 php3 9246 php3OLD 9258 ordtypelem2 9562 tcrank 9927 limsupgord 15474 isercoll 15672 isacs1i 17670 gsumzf1o 19910 dprdres 20028 dprd2da 20042 dmdprdsplit2lem 20045 lmhmlsp 21027 f1lindf 21820 iscnp4 23258 cnpco 23262 cncls2i 23265 cnntri 23266 cnrest2 23281 cnpresti 23283 cnprest 23284 1stcfb 23440 xkococnlem 23654 qtopval2 23691 tgqtop 23707 qtoprest 23712 kqdisj 23727 regr1lem 23734 kqreglem1 23736 kqreglem2 23737 kqnrmlem1 23738 kqnrmlem2 23739 nrmhmph 23789 fbasrn 23879 elfm2 23943 fmfnfmlem1 23949 fmco 23956 flffbas 23990 cnpflf2 23995 cnextcn 24062 metcnp3 24540 metustto 24553 cfilucfil 24559 uniioombllem3 25605 dyadmbllem 25619 mbfconstlem 25647 i1fima2 25699 itg2gt0 25781 ellimc3 25899 limcflf 25901 limcresi 25905 limciun 25914 lhop 26040 ig1peu 26202 ig1pdvds 26207 psercnlem2 26454 dvloglem 26675 efopn 26685 noetalem1 27771 madess 27900 cofcut1 27937 negsproplem2 28038 fnpreimac 32588 fsuppinisegfi 32599 gsumpart 32923 txomap 33649 zarcmplem 33696 tpr2rico 33727 pthhashvtx 34955 cvmsss2 35102 cvmopnlem 35106 cvmliftmolem1 35109 cvmliftlem15 35126 cvmlift2lem9 35139 imadifss 37296 poimirlem1 37322 poimirlem2 37323 poimirlem3 37324 poimirlem15 37336 poimirlem30 37351 dvtan 37371 heibor1lem 37510 aks6d1c2 41828 aks6d1c6lem3 41870 aks6d1c6lem5 41875 isnumbasabl 42767 isnumbasgrp 42768 dfacbasgrp 42769 trclimalb2 43393 frege81d 43414 imass2d 44871 limccog 45241 liminfgord 45375 uhgrimisgrgriclem 47477 clnbgrgrim 47481 |
Copyright terms: Public domain | W3C validator |