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

Theorem imass2 5370
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 5298 . . 3  |-  ( A 
C_  B  ->  ( C  |`  A )  C_  ( C  |`  B ) )
2 rnss 5229 . . 3  |-  ( ( C  |`  A )  C_  ( C  |`  B )  ->  ran  ( C  |`  A )  C_  ran  ( C  |`  B ) )
31, 2syl 16 . 2  |-  ( A 
C_  B  ->  ran  ( C  |`  A ) 
C_  ran  ( C  |`  B ) )
4 df-ima 5012 . 2  |-  ( C
" A )  =  ran  ( C  |`  A )
5 df-ima 5012 . 2  |-  ( C
" B )  =  ran  ( C  |`  B )
63, 4, 53sstr4g 3545 1  |-  ( A 
C_  B  ->  ( C " A )  C_  ( C " B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    C_ wss 3476   ran crn 5000    |` cres 5001   "cima 5002
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-br 4448  df-opab 4506  df-xp 5005  df-cnv 5007  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012
This theorem is referenced by:  funimass1  5659  funimass2  5660  fvimacnv  5994  f1imass  6158  ecinxp  7383  sbthlem1  7624  sbthlem2  7625  php3  7700  ordtypelem2  7940  mapfienOLD  8134  tcrank  8298  limsupgord  13254  isercoll  13449  isacs1i  14908  gsumzf1o  16708  gsumzf1oOLD  16711  dprdres  16865  dprd2da  16881  dmdprdsplit2lem  16884  lmhmlsp  17478  f1lindf  18624  iscnp4  19530  cnpco  19534  cncls2i  19537  cnntri  19538  cnrest2  19553  cnpresti  19555  cnprest  19556  1stcfb  19712  xkococnlem  19895  qtopval2  19932  tgqtop  19948  qtoprest  19953  kqdisj  19968  regr1lem  19975  kqreglem1  19977  kqreglem2  19978  kqnrmlem1  19979  kqnrmlem2  19980  nrmhmph  20030  fbasrn  20120  elfm2  20184  fmfnfmlem1  20190  fmco  20197  flffbas  20231  cnpflf2  20236  cnextcn  20302  metcnp3  20778  metusttoOLD  20795  metustto  20796  cfilucfilOLD  20807  cfilucfil  20808  uniioombllem3  21729  dyadmbllem  21743  mbfconstlem  21771  i1fima2  21821  itg2gt0  21902  ellimc3  22018  limcflf  22020  limcresi  22024  limciun  22033  lhop  22152  ig1peu  22307  ig1pdvds  22312  psercnlem2  22553  dvloglem  22757  efopn  22767  txomap  27500  tpr2rico  27530  cvmsss2  28359  cvmopnlem  28363  cvmliftmolem1  28366  cvmliftlem15  28383  cvmlift2lem9  28396  nofulllem3  29041  dvtan  29642  heibor1lem  29908  isnumbasabl  30659  isnumbasgrp  30660  dfacbasgrp  30661  limccog  31162
  Copyright terms: Public domain W3C validator