| 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 6022 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ↾ 𝐴) ⊆ (𝐶 ↾ 𝐵)) | |
| 2 | rnss 5950 | . . 3 ⊢ ((𝐶 ↾ 𝐴) ⊆ (𝐶 ↾ 𝐵) → ran (𝐶 ↾ 𝐴) ⊆ ran (𝐶 ↾ 𝐵)) | |
| 3 | 1, 2 | syl 17 | . 2 ⊢ (𝐴 ⊆ 𝐵 → ran (𝐶 ↾ 𝐴) ⊆ ran (𝐶 ↾ 𝐵)) |
| 4 | df-ima 5698 | . 2 ⊢ (𝐶 “ 𝐴) = ran (𝐶 ↾ 𝐴) | |
| 5 | df-ima 5698 | . 2 ⊢ (𝐶 “ 𝐵) = ran (𝐶 ↾ 𝐵) | |
| 6 | 3, 4, 5 | 3sstr4g 4037 | 1 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 “ 𝐴) ⊆ (𝐶 “ 𝐵)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ⊆ wss 3951 ran crn 5686 ↾ cres 5687 “ cima 5688 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-rab 3437 df-v 3482 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-nul 4334 df-if 4526 df-sn 4627 df-pr 4629 df-op 4633 df-br 5144 df-opab 5206 df-xp 5691 df-cnv 5693 df-dm 5695 df-rn 5696 df-res 5697 df-ima 5698 |
| This theorem is referenced by: funimass1 6648 funimass2 6649 fvimacnv 7073 fnfvimad 7254 f1imass 7284 ecinxp 8832 sbthlem1 9123 sbthlem2 9124 php3 9249 php3OLD 9261 ordtypelem2 9559 tcrank 9924 limsupgord 15508 isercoll 15704 isacs1i 17700 gsumzf1o 19930 dprdres 20048 dprd2da 20062 dmdprdsplit2lem 20065 lmhmlsp 21048 f1lindf 21842 iscnp4 23271 cnpco 23275 cncls2i 23278 cnntri 23279 cnrest2 23294 cnpresti 23296 cnprest 23297 1stcfb 23453 xkococnlem 23667 qtopval2 23704 tgqtop 23720 qtoprest 23725 kqdisj 23740 regr1lem 23747 kqreglem1 23749 kqreglem2 23750 kqnrmlem1 23751 kqnrmlem2 23752 nrmhmph 23802 fbasrn 23892 elfm2 23956 fmfnfmlem1 23962 fmco 23969 flffbas 24003 cnpflf2 24008 cnextcn 24075 metcnp3 24553 metustto 24566 cfilucfil 24572 uniioombllem3 25620 dyadmbllem 25634 mbfconstlem 25662 i1fima2 25714 itg2gt0 25795 ellimc3 25914 limcflf 25916 limcresi 25920 limciun 25929 lhop 26055 ig1peu 26214 ig1pdvds 26219 psercnlem2 26468 dvloglem 26690 efopn 26700 noetalem1 27786 madess 27915 cofcut1 27954 negsproplem2 28061 fnpreimac 32681 fsuppinisegfi 32696 gsumpart 33060 elrgspnsubrunlem2 33252 txomap 33833 zarcmplem 33880 tpr2rico 33911 pthhashvtx 35133 cvmsss2 35279 cvmopnlem 35283 cvmliftmolem1 35286 cvmliftlem15 35303 cvmlift2lem9 35316 imadifss 37602 poimirlem1 37628 poimirlem2 37629 poimirlem3 37630 poimirlem15 37642 poimirlem30 37657 dvtan 37677 heibor1lem 37816 aks6d1c2 42131 aks6d1c6lem3 42173 aks6d1c6lem5 42178 isnumbasabl 43118 isnumbasgrp 43119 dfacbasgrp 43120 trclimalb2 43739 frege81d 43760 imass2d 45268 limccog 45635 liminfgord 45769 uhgrimisgrgriclem 47898 clnbgrgrim 47902 |
| Copyright terms: Public domain | W3C validator |