Theorem imass1 5301

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 5234	. . 3 |- ( A C_ B -> ( A |` C ) C_ ( B |` C ) )
2		rnss 5166	. . 3 |- ( ( A |` C ) C_ ( B |` C ) -> ran ( A |` C ) C_ ran ( B |` C ) )
3	1, 2	syl 16	. 2 |- ( A C_ B -> ran ( A |` C ) C_ ran ( B |` C ) )
4		df-ima 4951	. 2 |- ( A " C ) = ran ( A |` C )
5		df-ima 4951	. 2 |- ( B " C ) = ran ( B |` C )
6	3, 4, 5	3sstr4g 3495	1 |- ( A C_ B -> ( A " C ) C_ ( B " C ) )

Syntax hints:   -> wi 4   C_ wss 3426   ran crn 4939   |` cres 4940   "cima 4941

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-rab 2804  df-v 3070  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-nul 3736  df-if 3890  df-sn 3976  df-pr 3978  df-op 3982  df-br 4391  df-opab 4449  df-cnv 4946  df-dm 4948  df-rn 4949  df-res 4950  df-ima 4951

This theorem is referenced by:  vdwnnlem1  14158  gsumzresOLD  16496  gsumzaddOLD  16515  gsum2dOLD  16569  dprdfaddOLD  16622  dprdres  16630  imasnopn  19379  imasncld  19380  imasncls  19381  tsmsresOLD  19833  utoptop  19925  restutop  19928  ustuqtop3  19934  utopreg  19943  metustblOLD  20271  metustbl  20272  imadifxp  26073  eulerpartlemmf  26892