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

Theorem imass2 5210
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 5137 . . 3  |-  ( A 
C_  B  ->  ( C  |`  A )  C_  ( C  |`  B ) )
2 rnss 5069 . . 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 4852 . 2  |-  ( C
" A )  =  ran  ( C  |`  A )
5 df-ima 4852 . 2  |-  ( C
" B )  =  ran  ( C  |`  B )
63, 4, 53sstr4g 3459 1  |-  ( A 
C_  B  ->  ( C " A )  C_  ( C " B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    C_ wss 3390   ran crn 4840    |` cres 4841   "cima 4842
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451
This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-rab 2765  df-v 3033  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-nul 3723  df-if 3873  df-sn 3960  df-pr 3962  df-op 3966  df-br 4396  df-opab 4455  df-xp 4845  df-cnv 4847  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852
This theorem is referenced by:  funimass1  5666  funimass2  5667  fvimacnv  6012  f1imass  6183  ecinxp  7456  sbthlem1  7700  sbthlem2  7701  php3  7776  ordtypelem2  8052  tcrank  8373  limsupgord  13605  isercoll  13808  isacs1i  15641  gsumzf1o  17624  dprdres  17739  dprd2da  17753  dmdprdsplit2lem  17756  lmhmlsp  18350  f1lindf  19457  iscnp4  20356  cnpco  20360  cncls2i  20363  cnntri  20364  cnrest2  20379  cnpresti  20381  cnprest  20382  1stcfb  20537  xkococnlem  20751  qtopval2  20788  tgqtop  20804  qtoprest  20809  kqdisj  20824  regr1lem  20831  kqreglem1  20833  kqreglem2  20834  kqnrmlem1  20835  kqnrmlem2  20836  nrmhmph  20886  fbasrn  20977  elfm2  21041  fmfnfmlem1  21047  fmco  21054  flffbas  21088  cnpflf2  21093  cnextcn  21160  metcnp3  21633  metustto  21646  cfilucfil  21652  uniioombllem3  22622  dyadmbllem  22636  mbfconstlem  22664  i1fima2  22716  itg2gt0  22797  ellimc3  22913  limcflf  22915  limcresi  22919  limciun  22928  lhop  23047  ig1peu  23201  ig1peuOLD  23202  ig1pdvds  23207  ig1pdvdsOLD  23213  psercnlem2  23458  dvloglem  23672  efopn  23682  txomap  28735  tpr2rico  28792  cvmsss2  30069  cvmopnlem  30073  cvmliftmolem1  30076  cvmliftlem15  30093  cvmlift2lem9  30106  nofulllem3  30664  imadifss  31992  poimirlem1  32005  poimirlem2  32006  poimirlem3  32007  poimirlem15  32019  poimirlem30  32034  dvtan  32056  heibor1lem  32205  isnumbasabl  36036  isnumbasgrp  36037  dfacbasgrp  36038  trclimalb2  36389  frege81d  36410  limccog  37797
  Copyright terms: Public domain W3C validator