![]() |
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 5970 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ↾ 𝐴) ⊆ (𝐶 ↾ 𝐵)) | |
2 | rnss 5899 | . . 3 ⊢ ((𝐶 ↾ 𝐴) ⊆ (𝐶 ↾ 𝐵) → ran (𝐶 ↾ 𝐴) ⊆ ran (𝐶 ↾ 𝐵)) | |
3 | 1, 2 | syl 17 | . 2 ⊢ (𝐴 ⊆ 𝐵 → ran (𝐶 ↾ 𝐴) ⊆ ran (𝐶 ↾ 𝐵)) |
4 | df-ima 5651 | . 2 ⊢ (𝐶 “ 𝐴) = ran (𝐶 ↾ 𝐴) | |
5 | df-ima 5651 | . 2 ⊢ (𝐶 “ 𝐵) = ran (𝐶 ↾ 𝐵) | |
6 | 3, 4, 5 | 3sstr4g 3994 | 1 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 “ 𝐴) ⊆ (𝐶 “ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ⊆ wss 3915 ran crn 5639 ↾ cres 5640 “ cima 5641 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2708 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2715 df-cleq 2729 df-clel 2815 df-rab 3411 df-v 3450 df-dif 3918 df-un 3920 df-in 3922 df-ss 3932 df-nul 4288 df-if 4492 df-sn 4592 df-pr 4594 df-op 4598 df-br 5111 df-opab 5173 df-xp 5644 df-cnv 5646 df-dm 5648 df-rn 5649 df-res 5650 df-ima 5651 |
This theorem is referenced by: funimass1 6588 funimass2 6589 fvimacnv 7008 fnfvimad 7189 f1imass 7216 ecinxp 8738 sbthlem1 9034 sbthlem2 9035 php3 9163 php3OLD 9175 ordtypelem2 9462 tcrank 9827 limsupgord 15361 isercoll 15559 isacs1i 17544 gsumzf1o 19696 dprdres 19814 dprd2da 19828 dmdprdsplit2lem 19831 lmhmlsp 20526 f1lindf 21244 iscnp4 22630 cnpco 22634 cncls2i 22637 cnntri 22638 cnrest2 22653 cnpresti 22655 cnprest 22656 1stcfb 22812 xkococnlem 23026 qtopval2 23063 tgqtop 23079 qtoprest 23084 kqdisj 23099 regr1lem 23106 kqreglem1 23108 kqreglem2 23109 kqnrmlem1 23110 kqnrmlem2 23111 nrmhmph 23161 fbasrn 23251 elfm2 23315 fmfnfmlem1 23321 fmco 23328 flffbas 23362 cnpflf2 23367 cnextcn 23434 metcnp3 23912 metustto 23925 cfilucfil 23931 uniioombllem3 24965 dyadmbllem 24979 mbfconstlem 25007 i1fima2 25059 itg2gt0 25141 ellimc3 25259 limcflf 25261 limcresi 25265 limciun 25274 lhop 25396 ig1peu 25552 ig1pdvds 25557 psercnlem2 25799 dvloglem 26019 efopn 26029 noetalem1 27105 madess 27228 cofcut1 27261 negsproplem2 27349 fnpreimac 31629 fsuppinisegfi 31644 gsumpart 31939 txomap 32455 zarcmplem 32502 tpr2rico 32533 pthhashvtx 33761 cvmsss2 33908 cvmopnlem 33912 cvmliftmolem1 33915 cvmliftlem15 33932 cvmlift2lem9 33945 imadifss 36082 poimirlem1 36108 poimirlem2 36109 poimirlem3 36110 poimirlem15 36122 poimirlem30 36137 dvtan 36157 heibor1lem 36297 isnumbasabl 41462 isnumbasgrp 41463 dfacbasgrp 41464 trclimalb2 42072 frege81d 42093 imass2d 43564 limccog 43935 liminfgord 44069 |
Copyright terms: Public domain | W3C validator |