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

Theorem imass2 5037
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 4970 . . 3  |-  ( A 
C_  B  ->  ( C  |`  A )  C_  ( C  |`  B ) )
2 rnss 4895 . . 3  |-  ( ( C  |`  A )  C_  ( C  |`  B )  ->  ran  (  C  |`  A )  C_  ran  (  C  |`  B ) )
31, 2syl 17 . 2  |-  ( A 
C_  B  ->  ran  (  C  |`  A ) 
C_  ran  (  C  |`  B ) )
4 df-ima 4682 . 2  |-  ( C
" A )  =  ran  (  C  |`  A )
5 df-ima 4682 . 2  |-  ( C
" B )  =  ran  (  C  |`  B )
63, 4, 53sstr4g 3194 1  |-  ( A 
C_  B  ->  ( C " A )  C_  ( C " B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6    C_ wss 3127   ran crn 4662    |` cres 4663   "cima 4664
This theorem is referenced by:  funimass1  5263  funimass2  5264  fvimacnv  5574  f1imass  5722  ecinxp  6702  sbthlem1  6939  sbthlem2  6940  php3  7015  ordtypelem2  7202  mapfien  7367  tcrank  7522  limsupgord  11912  isercoll  12107  isacs1i  13522  gsumzf1o  15159  dprdres  15226  dprd2da  15240  dmdprdsplit2lem  15243  lmhmlsp  15769  cnpco  16959  cncls2i  16962  cnntri  16963  cnrest2  16977  cnpresti  16979  cnprest  16980  1stcfb  17134  xkococnlem  17316  qtopval2  17350  tgqtop  17366  qtoprest  17371  kqdisj  17386  regr1lem  17393  kqreglem1  17395  kqreglem2  17396  kqnrmlem1  17397  kqnrmlem2  17398  nrmhmph  17448  fbasrn  17542  elfm2  17606  fmfnfmlem1  17612  fmco  17619  flffbas  17653  cnpflf2  17658  metcnp3  18049  uniioombllem3  18903  dyadmbllem  18917  mbfconstlem  18947  i1fima2  18997  itg2gt0  19078  ellimc3  19192  limcflf  19194  limcresi  19198  limciun  19207  lhop  19326  ig1peu  19520  ig1pdvds  19525  psercnlem2  19763  dvloglem  19958  efopn  19968  cvmsss2  23178  cvmopnlem  23182  cvmliftmolem1  23185  cvmliftlem15  23202  cvmlift2lem9  23215  axfelem13  23728  prjpacp1  24495  prjpacp2  24496  iscnp4  24931  limptlimpr2lem2  24943  lvsovso  24994  heibor1lem  25901  isnumbasabl  26639  isnumbasgrp  26640  dfacbasgrp  26641  f1lindf  26660
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2239
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-rab 2527  df-v 2765  df-dif 3130  df-un 3132  df-in 3134  df-ss 3141  df-nul 3431  df-if 3540  df-sn 3620  df-pr 3621  df-op 3623  df-br 3998  df-opab 4052  df-xp 4675  df-cnv 4677  df-dm 4679  df-rn 4680  df-res 4681  df-ima 4682
  Copyright terms: Public domain W3C validator