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

Theorem imass2 5204
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 5131 . . 3  |-  ( A 
C_  B  ->  ( C  |`  A )  C_  ( C  |`  B ) )
2 rnss 5063 . . 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 4847 . 2  |-  ( C
" A )  =  ran  ( C  |`  A )
5 df-ima 4847 . 2  |-  ( C
" B )  =  ran  ( C  |`  B )
63, 4, 53sstr4g 3473 1  |-  ( A 
C_  B  ->  ( C " A )  C_  ( C " B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    C_ wss 3404   ran crn 4835    |` cres 4836   "cima 4837
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-rab 2746  df-v 3047  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-nul 3732  df-if 3882  df-sn 3969  df-pr 3971  df-op 3975  df-br 4403  df-opab 4462  df-xp 4840  df-cnv 4842  df-dm 4844  df-rn 4845  df-res 4846  df-ima 4847
This theorem is referenced by:  funimass1  5656  funimass2  5657  fvimacnv  5997  f1imass  6165  ecinxp  7438  sbthlem1  7682  sbthlem2  7683  php3  7758  ordtypelem2  8034  tcrank  8355  limsupgord  13528  isercoll  13731  isacs1i  15563  gsumzf1o  17546  dprdres  17661  dprd2da  17675  dmdprdsplit2lem  17678  lmhmlsp  18272  f1lindf  19380  iscnp4  20279  cnpco  20283  cncls2i  20286  cnntri  20287  cnrest2  20302  cnpresti  20304  cnprest  20305  1stcfb  20460  xkococnlem  20674  qtopval2  20711  tgqtop  20727  qtoprest  20732  kqdisj  20747  regr1lem  20754  kqreglem1  20756  kqreglem2  20757  kqnrmlem1  20758  kqnrmlem2  20759  nrmhmph  20809  fbasrn  20899  elfm2  20963  fmfnfmlem1  20969  fmco  20976  flffbas  21010  cnpflf2  21015  cnextcn  21082  metcnp3  21555  metustto  21568  cfilucfil  21574  uniioombllem3  22543  dyadmbllem  22557  mbfconstlem  22585  i1fima2  22637  itg2gt0  22718  ellimc3  22834  limcflf  22836  limcresi  22840  limciun  22849  lhop  22968  ig1peu  23122  ig1peuOLD  23123  ig1pdvds  23128  ig1pdvdsOLD  23134  psercnlem2  23379  dvloglem  23593  efopn  23603  txomap  28661  tpr2rico  28718  cvmsss2  29997  cvmopnlem  30001  cvmliftmolem1  30004  cvmliftlem15  30021  cvmlift2lem9  30034  nofulllem3  30593  imadifss  31928  poimirlem1  31941  poimirlem2  31942  poimirlem3  31943  poimirlem15  31955  poimirlem30  31970  dvtan  31992  heibor1lem  32141  isnumbasabl  35965  isnumbasgrp  35966  dfacbasgrp  35967  trclimalb2  36318  frege81d  36339  limccog  37700
  Copyright terms: Public domain W3C validator