MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  imass2 Unicode version

Theorem imass2 5051
Description: Subset theorem for image. Exercise 22(a) of [Enderton] p. 53. (Contributed by NM, 22-Mar-1998.)
Assertion
Ref Expression
imass2  |-  ( A 
C_  B  ->  ( C " A )  C_  ( C " B ) )

Proof of Theorem imass2
StepHypRef Expression
1 ssres2 4984 . . 3  |-  ( A 
C_  B  ->  ( C  |`  A )  C_  ( C  |`  B ) )
2 rnss 4909 . . 3  |-  ( ( C  |`  A )  C_  ( C  |`  B )  ->  ran  ( C  |`  A )  C_  ran  ( C  |`  B ) )
31, 2syl 15 . 2  |-  ( A 
C_  B  ->  ran  ( C  |`  A ) 
C_  ran  ( C  |`  B ) )
4 df-ima 4704 . 2  |-  ( C
" A )  =  ran  ( C  |`  A )
5 df-ima 4704 . 2  |-  ( C
" B )  =  ran  ( C  |`  B )
63, 4, 53sstr4g 3221 1  |-  ( A 
C_  B  ->  ( C " A )  C_  ( C " B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    C_ wss 3154   ran crn 4692    |` cres 4693   "cima 4694
This theorem is referenced by:  funimass1  5327  funimass2  5328  fvimacnv  5642  f1imass  5790  ecinxp  6736  sbthlem1  6973  sbthlem2  6974  php3  7049  ordtypelem2  7236  mapfien  7401  tcrank  7556  limsupgord  11948  isercoll  12143  isacs1i  13561  gsumzf1o  15198  dprdres  15265  dprd2da  15279  dmdprdsplit2lem  15282  lmhmlsp  15808  cnpco  16998  cncls2i  17001  cnntri  17002  cnrest2  17016  cnpresti  17018  cnprest  17019  1stcfb  17173  xkococnlem  17355  qtopval2  17389  tgqtop  17405  qtoprest  17410  kqdisj  17425  regr1lem  17432  kqreglem1  17434  kqreglem2  17435  kqnrmlem1  17436  kqnrmlem2  17437  nrmhmph  17487  fbasrn  17581  elfm2  17645  fmfnfmlem1  17651  fmco  17658  flffbas  17692  cnpflf2  17697  metcnp3  18088  uniioombllem3  18942  dyadmbllem  18956  mbfconstlem  18986  i1fima2  19036  itg2gt0  19117  ellimc3  19231  limcflf  19233  limcresi  19237  limciun  19246  lhop  19365  ig1peu  19559  ig1pdvds  19564  psercnlem2  19802  dvloglem  19997  efopn  20007  cvmsss2  23807  cvmopnlem  23811  cvmliftmolem1  23814  cvmliftlem15  23831  cvmlift2lem9  23844  nofulllem3  24360  prjpacp1  25138  prjpacp2  25139  iscnp4  25574  limptlimpr2lem2  25586  lvsovso  25637  heibor1lem  26544  isnumbasabl  27282  isnumbasgrp  27283  dfacbasgrp  27284  f1lindf  27303
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-rab 2554  df-v 2792  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-nul 3458  df-if 3568  df-sn 3648  df-pr 3649  df-op 3651  df-br 4026  df-opab 4080  df-xp 4697  df-cnv 4699  df-dm 4701  df-rn 4702  df-res 4703  df-ima 4704
  Copyright terms: Public domain W3C validator