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

Theorem imass2 5048
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 4981 . . 3  |-  ( A 
C_  B  ->  ( C  |`  A )  C_  ( C  |`  B ) )
2 rnss 4906 . . 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 4701 . 2  |-  ( C
" A )  =  ran  (  C  |`  A )
5 df-ima 4701 . 2  |-  ( C
" B )  =  ran  (  C  |`  B )
63, 4, 53sstr4g 3220 1  |-  ( A 
C_  B  ->  ( C " A )  C_  ( C " B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    C_ wss 3153   ran crn 4689    |` cres 4690   "cima 4691
This theorem is referenced by:  funimass1  5291  funimass2  5292  fvimacnv  5602  f1imass  5750  ecinxp  6730  sbthlem1  6967  sbthlem2  6968  php3  7043  ordtypelem2  7230  mapfien  7395  tcrank  7550  limsupgord  11942  isercoll  12137  isacs1i  13555  gsumzf1o  15192  dprdres  15259  dprd2da  15273  dmdprdsplit2lem  15276  lmhmlsp  15802  cnpco  16992  cncls2i  16995  cnntri  16996  cnrest2  17010  cnpresti  17012  cnprest  17013  1stcfb  17167  xkococnlem  17349  qtopval2  17383  tgqtop  17399  qtoprest  17404  kqdisj  17419  regr1lem  17426  kqreglem1  17428  kqreglem2  17429  kqnrmlem1  17430  kqnrmlem2  17431  nrmhmph  17481  fbasrn  17575  elfm2  17639  fmfnfmlem1  17645  fmco  17652  flffbas  17686  cnpflf2  17691  metcnp3  18082  uniioombllem3  18936  dyadmbllem  18950  mbfconstlem  18980  i1fima2  19030  itg2gt0  19111  ellimc3  19225  limcflf  19227  limcresi  19231  limciun  19240  lhop  19359  ig1peu  19553  ig1pdvds  19558  psercnlem2  19796  dvloglem  19991  efopn  20001  cvmsss2  23212  cvmopnlem  23216  cvmliftmolem1  23219  cvmliftlem15  23236  cvmlift2lem9  23249  axfelem13  23762  prjpacp1  24538  prjpacp2  24539  iscnp4  24974  limptlimpr2lem2  24986  lvsovso  25037  heibor1lem  25944  isnumbasabl  26682  isnumbasgrp  26683  dfacbasgrp  26684  f1lindf  26703
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1636  ax-8 1644  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2265
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1631  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-rab 2553  df-v 2791  df-dif 3156  df-un 3158  df-in 3160  df-ss 3167  df-nul 3457  df-if 3567  df-sn 3647  df-pr 3648  df-op 3650  df-br 4025  df-opab 4079  df-xp 4694  df-cnv 4696  df-dm 4698  df-rn 4699  df-res 4700  df-ima 4701
  Copyright terms: Public domain W3C validator