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

Step	Hyp	Ref	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 ) )
3	1, 2	syl 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 )
6	3, 4, 5	3sstr4g 3440	1 |- ( A C_ B -> ( A " C ) C_ ( B " C ) )

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