Theorem imass2 6088

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 5988	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ↾ 𝐴) ⊆ (𝐶 ↾ 𝐵))
2		rnss 5913	. . 3 ⊢ ((𝐶 ↾ 𝐴) ⊆ (𝐶 ↾ 𝐵) → ran (𝐶 ↾ 𝐴) ⊆ ran (𝐶 ↾ 𝐵))
3	1, 2	syl 17	. 2 ⊢ (𝐴 ⊆ 𝐵 → ran (𝐶 ↾ 𝐴) ⊆ ran (𝐶 ↾ 𝐵))
4		df-ima 5658	. 2 ⊢ (𝐶 “ 𝐴) = ran (𝐶 ↾ 𝐴)
5		df-ima 5658	. 2 ⊢ (𝐶 “ 𝐵) = ran (𝐶 ↾ 𝐵)
6	3, 4, 5	3sstr4g 3989	1 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 “ 𝐴) ⊆ (𝐶 “ 𝐵))

Syntax hints:   → wi 4   ⊆ wss 3904  ran crn 5646   ↾ cres 5647   “ cima 5648

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4480  df-sn 4582  df-pr 4584  df-op 4588  df-br 5100  df-opab 5162  df-xp 5651  df-cnv 5653  df-dm 5655  df-rn 5656  df-res 5657  df-ima 5658

This theorem is referenced by:  funimass1  6599  funimass2  6600  fvimacnv  7030  fnfvimad  7214  f1imass  7244  ecinxp  8769  sbthlem1  9055  sbthlem2  9056  php3  9173  ordtypelem2  9464  tcrank  9839  limsupgord  15482  isercoll  15678  isacs1i  17672  gsumzf1o  19935  dprdres  20053  dprd2da  20067  dmdprdsplit2lem  20070  lmhmlsp  21096  f1lindf  21854  iscnp4  23303  cnpco  23307  cncls2i  23310  cnntri  23311  cnrest2  23326  cnpresti  23328  cnprest  23329  1stcfb  23485  xkococnlem  23699  qtopval2  23736  tgqtop  23752  qtoprest  23757  kqdisj  23772  regr1lem  23779  kqreglem1  23781  kqreglem2  23782  kqnrmlem1  23783  kqnrmlem2  23784  nrmhmph  23834  fbasrn  23924  elfm2  23988  fmfnfmlem1  23994  fmco  24001  flffbas  24035  cnpflf2  24040  cnextcn  24107  metcnp3  24580  metustto  24593  cfilucfil  24599  uniioombllem3  25627  dyadmbllem  25641  mbfconstlem  25669  i1fima2  25721  itg2gt0  25802  ellimc3  25921  limcflf  25923  limcresi  25927  limciun  25936  lhop  26058  ig1peu  26215  ig1pdvds  26220  psercnlem2  26464  dvloglem  26690  efopn  26700  noetalem1  27782  madess  27936  oldss  27940  cofcut1  27990  negsproplem2  28099  bdayons  28346  fnpreimac  32822  fsuppinisegfi  32839  gsumpart  33204  elrgspnsubrunlem2  33390  txomap  34092  zarcmplem  34139  tpr2rico  34170  pthhashvtx  35442  cvmsss2  35588  cvmopnlem  35592  cvmliftmolem1  35595  cvmliftlem15  35612  cvmlift2lem9  35625  imadifss  38058  poimirlem1  38084  poimirlem2  38085  poimirlem3  38086  poimirlem15  38098  poimirlem30  38113  dvtan  38133  heibor1lem  38272  aks6d1c2  42711  aks6d1c6lem3  42753  aks6d1c6lem5  42758  isnumbasabl  43647  isnumbasgrp  43648  dfacbasgrp  43649  trclimalb2  44266  frege81d  44287  imass2d  45800  limccog  46160  liminfgord  46292  uhgrimisgrgriclem  48516  clnbgrgrim  48520