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

Theorem imass1 5180
Description: Subset theorem for image. (Contributed by NM, 16-Mar-2004.)
Assertion
Ref Expression
imass1  |-  ( A 
C_  B  ->  ( A " C )  C_  ( B " C ) )

Proof of Theorem imass1
StepHypRef Expression
1 ssres 5107 . . 3  |-  ( A 
C_  B  ->  ( A  |`  C )  C_  ( B  |`  C ) )
2 rnss 5040 . . 3  |-  ( ( A  |`  C )  C_  ( B  |`  C )  ->  ran  ( A  |`  C )  C_  ran  ( B  |`  C ) )
31, 2syl 17 . 2  |-  ( A 
C_  B  ->  ran  ( A  |`  C ) 
C_  ran  ( B  |`  C ) )
4 df-ima 4824 . 2  |-  ( A
" C )  =  ran  ( A  |`  C )
5 df-ima 4824 . 2  |-  ( B
" C )  =  ran  ( B  |`  C )
63, 4, 53sstr4g 3440 1  |-  ( A 
C_  B  ->  ( A " C )  C_  ( B " C ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    C_ wss 3371   ran crn 4812    |` cres 4813   "cima 4814
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1672  ax-4 1685  ax-5 1761  ax-6 1808  ax-7 1854  ax-10 1918  ax-11 1923  ax-12 1936  ax-13 2091  ax-ext 2431
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 988  df-tru 1450  df-ex 1667  df-nf 1671  df-sb 1801  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-rab 2745  df-v 3014  df-dif 3374  df-un 3376  df-in 3378  df-ss 3385  df-nul 3699  df-if 3849  df-sn 3936  df-pr 3938  df-op 3942  df-br 4374  df-opab 4433  df-cnv 4819  df-dm 4821  df-rn 4822  df-res 4823  df-ima 4824
This theorem is referenced by:  vdwnnlem1  14955  dprdres  17671  imasnopn  20715  imasncld  20716  imasncls  20717  utoptop  21259  restutop  21262  ustuqtop3  21268  utopreg  21277  metustbl  21591  imadifxp  28220  esum2d  28920  eulerpartlemmf  29213  brtrclfv2  36320  frege97d  36345  frege109d  36350  frege131d  36357  hess  36376
  Copyright terms: Public domain W3C validator