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

Theorem imass2 5152
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 5085 . . 3  |-  ( A 
C_  B  ->  ( C  |`  A )  C_  ( C  |`  B ) )
2 rnss 5010 . . 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 4805 . 2  |-  ( C
" A )  =  ran  ( C  |`  A )
5 df-ima 4805 . 2  |-  ( C
" B )  =  ran  ( C  |`  B )
63, 4, 53sstr4g 3305 1  |-  ( A 
C_  B  ->  ( C " A )  C_  ( C " B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    C_ wss 3238   ran crn 4793    |` cres 4794   "cima 4795
This theorem is referenced by:  funimass1  5430  funimass2  5431  fvimacnv  5747  f1imass  5910  ecinxp  6876  sbthlem1  7114  sbthlem2  7115  php3  7190  ordtypelem2  7381  mapfien  7546  tcrank  7701  limsupgord  12153  isercoll  12348  isacs1i  13769  gsumzf1o  15406  dprdres  15473  dprd2da  15487  dmdprdsplit2lem  15490  lmhmlsp  16016  cnpco  17213  cncls2i  17216  cnntri  17217  cnrest2  17231  cnpresti  17233  cnprest  17234  1stcfb  17388  xkococnlem  17570  qtopval2  17604  tgqtop  17620  qtoprest  17625  kqdisj  17640  regr1lem  17647  kqreglem1  17649  kqreglem2  17650  kqnrmlem1  17651  kqnrmlem2  17652  nrmhmph  17702  fbasrn  17792  elfm2  17856  fmfnfmlem1  17862  fmco  17869  flffbas  17903  cnpflf2  17908  metcnp3  18299  uniioombllem3  19155  dyadmbllem  19169  mbfconstlem  19199  i1fima2  19249  itg2gt0  19330  ellimc3  19444  limcflf  19446  limcresi  19450  limciun  19459  lhop  19578  ig1peu  19772  ig1pdvds  19777  psercnlem2  20018  dvloglem  20217  efopn  20227  iscnp4  23646  cnextcn  23703  metustto  23796  cfilucfil  23802  cvmsss2  24408  cvmopnlem  24412  cvmliftmolem1  24415  cvmliftlem15  24432  cvmlift2lem9  24445  nofulllem3  25099  heibor1lem  26039  isnumbasabl  26777  isnumbasgrp  26778  dfacbasgrp  26779  f1lindf  26798
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 937  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-clab 2353  df-cleq 2359  df-clel 2362  df-nfc 2491  df-rab 2637  df-v 2875  df-dif 3241  df-un 3243  df-in 3245  df-ss 3252  df-nul 3544  df-if 3655  df-sn 3735  df-pr 3736  df-op 3738  df-br 4126  df-opab 4180  df-xp 4798  df-cnv 4800  df-dm 4802  df-rn 4803  df-res 4804  df-ima 4805
  Copyright terms: Public domain W3C validator