| 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 5963 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ↾ 𝐴) ⊆ (𝐶 ↾ 𝐵)) | |
| 2 | rnss 5888 | . . 3 ⊢ ((𝐶 ↾ 𝐴) ⊆ (𝐶 ↾ 𝐵) → ran (𝐶 ↾ 𝐴) ⊆ ran (𝐶 ↾ 𝐵)) | |
| 3 | 1, 2 | syl 17 | . 2 ⊢ (𝐴 ⊆ 𝐵 → ran (𝐶 ↾ 𝐴) ⊆ ran (𝐶 ↾ 𝐵)) |
| 4 | df-ima 5637 | . 2 ⊢ (𝐶 “ 𝐴) = ran (𝐶 ↾ 𝐴) | |
| 5 | df-ima 5637 | . 2 ⊢ (𝐶 “ 𝐵) = ran (𝐶 ↾ 𝐵) | |
| 6 | 3, 4, 5 | 3sstr4g 3987 | 1 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 “ 𝐴) ⊆ (𝐶 “ 𝐵)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ⊆ wss 3901 ran crn 5625 ↾ cres 5626 “ cima 5627 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-sb 2068 df-clab 2715 df-cleq 2728 df-clel 2811 df-rab 3400 df-v 3442 df-dif 3904 df-un 3906 df-in 3908 df-ss 3918 df-nul 4286 df-if 4480 df-sn 4581 df-pr 4583 df-op 4587 df-br 5099 df-opab 5161 df-xp 5630 df-cnv 5632 df-dm 5634 df-rn 5635 df-res 5636 df-ima 5637 |
| This theorem is referenced by: funimass1 6574 funimass2 6575 fvimacnv 6998 fnfvimad 7180 f1imass 7210 ecinxp 8729 sbthlem1 9015 sbthlem2 9016 php3 9133 ordtypelem2 9424 tcrank 9796 limsupgord 15395 isercoll 15591 isacs1i 17580 gsumzf1o 19841 dprdres 19959 dprd2da 19973 dmdprdsplit2lem 19976 lmhmlsp 21001 f1lindf 21777 iscnp4 23207 cnpco 23211 cncls2i 23214 cnntri 23215 cnrest2 23230 cnpresti 23232 cnprest 23233 1stcfb 23389 xkococnlem 23603 qtopval2 23640 tgqtop 23656 qtoprest 23661 kqdisj 23676 regr1lem 23683 kqreglem1 23685 kqreglem2 23686 kqnrmlem1 23687 kqnrmlem2 23688 nrmhmph 23738 fbasrn 23828 elfm2 23892 fmfnfmlem1 23898 fmco 23905 flffbas 23939 cnpflf2 23944 cnextcn 24011 metcnp3 24484 metustto 24497 cfilucfil 24503 uniioombllem3 25542 dyadmbllem 25556 mbfconstlem 25584 i1fima2 25636 itg2gt0 25717 ellimc3 25836 limcflf 25838 limcresi 25842 limciun 25851 lhop 25977 ig1peu 26136 ig1pdvds 26141 psercnlem2 26390 dvloglem 26613 efopn 26623 noetalem1 27709 madess 27862 oldss 27866 cofcut1 27916 negsproplem2 28025 bdayons 28272 fnpreimac 32749 fsuppinisegfi 32766 gsumpart 33146 elrgspnsubrunlem2 33330 txomap 33991 zarcmplem 34038 tpr2rico 34069 pthhashvtx 35322 cvmsss2 35468 cvmopnlem 35472 cvmliftmolem1 35475 cvmliftlem15 35492 cvmlift2lem9 35505 imadifss 37792 poimirlem1 37818 poimirlem2 37819 poimirlem3 37820 poimirlem15 37832 poimirlem30 37847 dvtan 37867 heibor1lem 38006 aks6d1c2 42380 aks6d1c6lem3 42422 aks6d1c6lem5 42427 isnumbasabl 43344 isnumbasgrp 43345 dfacbasgrp 43346 trclimalb2 43963 frege81d 43984 imass2d 45501 limccog 45862 liminfgord 45994 uhgrimisgrgriclem 48172 clnbgrgrim 48176 |
| Copyright terms: Public domain | W3C validator |