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

Theorem imass2 5194
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 5122 . . 3  |-  ( A 
C_  B  ->  ( C  |`  A )  C_  ( C  |`  B ) )
2 rnss 5054 . . 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 4838 . 2  |-  ( C
" A )  =  ran  ( C  |`  A )
5 df-ima 4838 . 2  |-  ( C
" B )  =  ran  ( C  |`  B )
63, 4, 53sstr4g 3485 1  |-  ( A 
C_  B  ->  ( C " A )  C_  ( C " B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    C_ wss 3416   ran crn 4826    |` cres 4827   "cima 4828
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1641  ax-4 1654  ax-5 1727  ax-6 1773  ax-7 1816  ax-10 1863  ax-11 1868  ax-12 1880  ax-13 2028  ax-ext 2382
This theorem depends on definitions:  df-bi 187  df-or 370  df-an 371  df-3an 978  df-tru 1410  df-ex 1636  df-nf 1640  df-sb 1766  df-clab 2390  df-cleq 2396  df-clel 2399  df-nfc 2554  df-rab 2765  df-v 3063  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3741  df-if 3888  df-sn 3975  df-pr 3977  df-op 3981  df-br 4398  df-opab 4456  df-xp 4831  df-cnv 4833  df-dm 4835  df-rn 4836  df-res 4837  df-ima 4838
This theorem is referenced by:  funimass1  5644  funimass2  5645  fvimacnv  5982  f1imass  6155  ecinxp  7425  sbthlem1  7667  sbthlem2  7668  php3  7743  ordtypelem2  7980  mapfienOLD  8172  tcrank  8336  limsupgord  13446  isercoll  13641  isacs1i  15273  gsumzf1o  17243  gsumzf1oOLD  17246  dprdres  17397  dprd2da  17413  dmdprdsplit2lem  17416  lmhmlsp  18017  f1lindf  19151  iscnp4  20059  cnpco  20063  cncls2i  20066  cnntri  20067  cnrest2  20082  cnpresti  20084  cnprest  20085  1stcfb  20240  xkococnlem  20454  qtopval2  20491  tgqtop  20507  qtoprest  20512  kqdisj  20527  regr1lem  20534  kqreglem1  20536  kqreglem2  20537  kqnrmlem1  20538  kqnrmlem2  20539  nrmhmph  20589  fbasrn  20679  elfm2  20743  fmfnfmlem1  20749  fmco  20756  flffbas  20790  cnpflf2  20795  cnextcn  20861  metcnp3  21337  metusttoOLD  21354  metustto  21355  cfilucfilOLD  21366  cfilucfil  21367  uniioombllem3  22288  dyadmbllem  22302  mbfconstlem  22330  i1fima2  22380  itg2gt0  22461  ellimc3  22577  limcflf  22579  limcresi  22583  limciun  22592  lhop  22711  ig1peu  22866  ig1pdvds  22871  psercnlem2  23113  dvloglem  23325  efopn  23335  txomap  28303  tpr2rico  28360  cvmsss2  29584  cvmopnlem  29588  cvmliftmolem1  29591  cvmliftlem15  29608  cvmlift2lem9  29621  nofulllem3  30177  dvtan  31451  heibor1lem  31600  isnumbasabl  35432  isnumbasgrp  35433  dfacbasgrp  35434  trclimalb2  35718  frege81d  35739  limccog  37007
  Copyright terms: Public domain W3C validator