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

Theorem imass2 5199
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 5132 . . 3  |-  ( A 
C_  B  ->  ( C  |`  A )  C_  ( C  |`  B ) )
2 rnss 5057 . . 3  |-  ( ( C  |`  A )  C_  ( C  |`  B )  ->  ran  ( C  |`  A )  C_  ran  ( C  |`  B ) )
31, 2syl 16 . 2  |-  ( A 
C_  B  ->  ran  ( C  |`  A ) 
C_  ran  ( C  |`  B ) )
4 df-ima 4850 . 2  |-  ( C
" A )  =  ran  ( C  |`  A )
5 df-ima 4850 . 2  |-  ( C
" B )  =  ran  ( C  |`  B )
63, 4, 53sstr4g 3349 1  |-  ( A 
C_  B  ->  ( C " A )  C_  ( C " B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    C_ wss 3280   ran crn 4838    |` cres 4839   "cima 4840
This theorem is referenced by:  funimass1  5485  funimass2  5486  fvimacnv  5804  f1imass  5969  ecinxp  6938  sbthlem1  7176  sbthlem2  7177  php3  7252  ordtypelem2  7444  mapfien  7609  tcrank  7764  limsupgord  12221  isercoll  12416  isacs1i  13837  gsumzf1o  15474  dprdres  15541  dprd2da  15555  dmdprdsplit2lem  15558  lmhmlsp  16080  iscnp4  17281  cnpco  17285  cncls2i  17288  cnntri  17289  cnrest2  17304  cnpresti  17306  cnprest  17307  1stcfb  17461  xkococnlem  17644  qtopval2  17681  tgqtop  17697  qtoprest  17702  kqdisj  17717  regr1lem  17724  kqreglem1  17726  kqreglem2  17727  kqnrmlem1  17728  kqnrmlem2  17729  nrmhmph  17779  fbasrn  17869  elfm2  17933  fmfnfmlem1  17939  fmco  17946  flffbas  17980  cnpflf2  17985  cnextcn  18051  metcnp3  18523  metusttoOLD  18540  metustto  18541  cfilucfilOLD  18552  cfilucfil  18553  uniioombllem3  19430  dyadmbllem  19444  mbfconstlem  19474  i1fima2  19524  itg2gt0  19605  ellimc3  19719  limcflf  19721  limcresi  19725  limciun  19734  lhop  19853  ig1peu  20047  ig1pdvds  20052  psercnlem2  20293  dvloglem  20492  efopn  20502  tpr2rico  24263  cvmsss2  24914  cvmopnlem  24918  cvmliftmolem1  24921  cvmliftlem15  24938  cvmlift2lem9  24951  nofulllem3  25572  heibor1lem  26408  isnumbasabl  27139  isnumbasgrp  27140  dfacbasgrp  27141  f1lindf  27160
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-br 4173  df-opab 4227  df-xp 4843  df-cnv 4845  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850
  Copyright terms: Public domain W3C validator