Theorem imass2 5932

Description: Subset theorem for image. Exercise 22(a) of [Enderton] p. 53. (Contributed by NM, 22-Mar-1998.)

Assertion

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

Proof of Theorem imass2

Step	Hyp	Ref	Expression
1		ssres2 5846	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ↾ 𝐴) ⊆ (𝐶 ↾ 𝐵))
2		rnss 5773	. . 3 ⊢ ((𝐶 ↾ 𝐴) ⊆ (𝐶 ↾ 𝐵) → ran (𝐶 ↾ 𝐴) ⊆ ran (𝐶 ↾ 𝐵))
3	1, 2	syl 17	. 2 ⊢ (𝐴 ⊆ 𝐵 → ran (𝐶 ↾ 𝐴) ⊆ ran (𝐶 ↾ 𝐵))
4		df-ima 5532	. 2 ⊢ (𝐶 “ 𝐴) = ran (𝐶 ↾ 𝐴)
5		df-ima 5532	. 2 ⊢ (𝐶 “ 𝐵) = ran (𝐶 ↾ 𝐵)
6	3, 4, 5	3sstr4g 3960	1 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 “ 𝐴) ⊆ (𝐶 “ 𝐵))

Syntax hints:   → wi 4   ⊆ wss 3881  ran crn 5520   ↾ cres 5521   “ cima 5522

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-rab 3115  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-sn 4526  df-pr 4528  df-op 4532  df-br 5031  df-opab 5093  df-xp 5525  df-cnv 5527  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532

This theorem is referenced by:  funimass1  6406  funimass2  6407  fvimacnv  6800  fnfvimad  6974  f1imass  7000  ecinxp  8355  sbthlem1  8611  sbthlem2  8612  php3  8687  ordtypelem2  8967  tcrank  9297  limsupgord  14821  isercoll  15016  isacs1i  16920  gsumzf1o  19025  dprdres  19143  dprd2da  19157  dmdprdsplit2lem  19160  lmhmlsp  19814  f1lindf  20511  iscnp4  21868  cnpco  21872  cncls2i  21875  cnntri  21876  cnrest2  21891  cnpresti  21893  cnprest  21894  1stcfb  22050  xkococnlem  22264  qtopval2  22301  tgqtop  22317  qtoprest  22322  kqdisj  22337  regr1lem  22344  kqreglem1  22346  kqreglem2  22347  kqnrmlem1  22348  kqnrmlem2  22349  nrmhmph  22399  fbasrn  22489  elfm2  22553  fmfnfmlem1  22559  fmco  22566  flffbas  22600  cnpflf2  22605  cnextcn  22672  metcnp3  23147  metustto  23160  cfilucfil  23166  uniioombllem3  24189  dyadmbllem  24203  mbfconstlem  24231  i1fima2  24283  itg2gt0  24364  ellimc3  24482  limcflf  24484  limcresi  24488  limciun  24497  lhop  24619  ig1peu  24772  ig1pdvds  24777  psercnlem2  25019  dvloglem  25239  efopn  25249  fnpreimac  30434  fsuppinisegfi  30447  gsumpart  30740  txomap  31187  zarcmplem  31234  tpr2rico  31265  pthhashvtx  32487  cvmsss2  32634  cvmopnlem  32638  cvmliftmolem1  32641  cvmliftlem15  32658  cvmlift2lem9  32671  imadifss  35032  poimirlem1  35058  poimirlem2  35059  poimirlem3  35060  poimirlem15  35072  poimirlem30  35087  dvtan  35107  heibor1lem  35247  isnumbasabl  40050  isnumbasgrp  40051  dfacbasgrp  40052  trclimalb2  40427  frege81d  40448  imass2d  41901  limccog  42262  liminfgord  42396