Theorem imass1 6075

Description: Subset theorem for image. (Contributed by NM, 16-Mar-2004.)

Assertion

Ref	Expression
imass1	⊢ (𝐴 ⊆ 𝐵 → (𝐴 “ 𝐶) ⊆ (𝐵 “ 𝐶))

Proof of Theorem imass1

Step	Hyp	Ref	Expression
1		ssres 5977	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ↾ 𝐶) ⊆ (𝐵 ↾ 𝐶))
2		rnss 5906	. . 3 ⊢ ((𝐴 ↾ 𝐶) ⊆ (𝐵 ↾ 𝐶) → ran (𝐴 ↾ 𝐶) ⊆ ran (𝐵 ↾ 𝐶))
3	1, 2	syl 17	. 2 ⊢ (𝐴 ⊆ 𝐵 → ran (𝐴 ↾ 𝐶) ⊆ ran (𝐵 ↾ 𝐶))
4		df-ima 5654	. 2 ⊢ (𝐴 “ 𝐶) = ran (𝐴 ↾ 𝐶)
5		df-ima 5654	. 2 ⊢ (𝐵 “ 𝐶) = ran (𝐵 ↾ 𝐶)
6	3, 4, 5	3sstr4g 4003	1 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 “ 𝐶) ⊆ (𝐵 “ 𝐶))

Syntax hints:   → wi 4   ⊆ wss 3917  ran crn 5642   ↾ cres 5643   “ cima 5644

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111  df-opab 5173  df-cnv 5649  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654

This theorem is referenced by:  predrelss  6313  vdwnnlem1  16973  dprdres  19967  imasnopn  23584  imasncld  23585  imasncls  23586  utoptop  24129  restutop  24132  ustuqtop3  24138  utopreg  24147  metustbl  24461  imadifxp  32537  gsumfs2d  33002  esum2d  34090  eulerpartlemmf  34373  bj-imdirco  37185  brtrclfv2  43723  frege97d  43748  frege109d  43753  frege131d  43760  hess  43776  resimass  45241  setrecsss  49694