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

Theorem imass2 4956
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 4889 . . 3  |-  ( A 
C_  B  ->  ( C  |`  A )  C_  ( C  |`  B ) )
2 rnss 4814 . . 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 4601 . 2  |-  ( C
" A )  =  ran  (  C  |`  A )
5 df-ima 4601 . 2  |-  ( C
" B )  =  ran  (  C  |`  B )
63, 4, 53sstr4g 3140 1  |-  ( A 
C_  B  ->  ( C " A )  C_  ( C " B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6    C_ wss 3078   ran crn 4581    |` cres 4582   "cima 4583
This theorem is referenced by:  funimass1  5182  funimass2  5183  fvimacnv  5492  f1imass  5640  ecinxp  6620  sbthlem1  6856  sbthlem2  6857  php3  6932  ordtypelem2  7118  mapfien  7283  tcrank  7438  limsupgord  11823  isercoll  12018  isacs1i  13403  gsumzf1o  15031  dprdres  15098  dprd2da  15112  dmdprdsplit2lem  15115  lmhmlsp  15641  cnpco  16828  cncls2i  16831  cnntri  16832  cnrest2  16846  cnpresti  16848  cnprest  16849  1stcfb  17003  xkococnlem  17185  qtopval2  17219  tgqtop  17235  qtoprest  17240  kqdisj  17255  regr1lem  17262  kqreglem1  17264  kqreglem2  17265  kqnrmlem1  17266  kqnrmlem2  17267  nrmhmph  17317  fbasrn  17411  elfm2  17475  fmfnfmlem1  17481  fmco  17488  flffbas  17522  cnpflf2  17527  metcnp3  17918  uniioombllem3  18772  dyadmbllem  18786  mbfconstlem  18816  i1fima2  18866  itg2gt0  18947  ellimc3  19061  limcflf  19063  limcresi  19067  limciun  19076  lhop  19195  ig1peu  19389  ig1pdvds  19394  psercnlem2  19632  dvloglem  19827  efopn  19837  cvmsss2  22976  cvmopnlem  22980  cvmliftmolem1  22983  cvmliftlem15  23000  cvmlift2lem9  23013  axfelem13  23526  prjpacp1  24293  prjpacp2  24294  iscnp4  24729  limptlimpr2lem2  24741  lvsovso  24792  heibor1lem  25699  isnumbasabl  26437  isnumbasgrp  26438  dfacbasgrp  26439  f1lindf  26458
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 1926  ax-ext 2234
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 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-rab 2516  df-v 2729  df-dif 3081  df-un 3083  df-in 3085  df-ss 3089  df-nul 3363  df-if 3471  df-sn 3550  df-pr 3551  df-op 3553  df-br 3921  df-opab 3975  df-xp 4594  df-cnv 4596  df-dm 4598  df-rn 4599  df-res 4600  df-ima 4601
  Copyright terms: Public domain W3C validator