Theorem imass2 6061

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

Syntax hints:   → wi 4   ⊆ wss 3890  ran crn 5626   ↾ cres 5627   “ cima 5628

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-br 5080  df-opab 5142  df-xp 5631  df-cnv 5633  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638

This theorem is referenced by:  funimass1  6574  funimass2  6575  fvimacnv  7001  fnfvimad  7185  f1imass  7215  ecinxp  8736  sbthlem1  9022  sbthlem2  9023  php3  9140  ordtypelem2  9431  tcrank  9806  limsupgord  15432  isercoll  15628  isacs1i  17621  gsumzf1o  19885  dprdres  20003  dprd2da  20017  dmdprdsplit2lem  20020  lmhmlsp  21046  f1lindf  21804  iscnp4  23253  cnpco  23257  cncls2i  23260  cnntri  23261  cnrest2  23276  cnpresti  23278  cnprest  23279  1stcfb  23435  xkococnlem  23649  qtopval2  23686  tgqtop  23702  qtoprest  23707  kqdisj  23722  regr1lem  23729  kqreglem1  23731  kqreglem2  23732  kqnrmlem1  23733  kqnrmlem2  23734  nrmhmph  23784  fbasrn  23874  elfm2  23938  fmfnfmlem1  23944  fmco  23951  flffbas  23985  cnpflf2  23990  cnextcn  24057  metcnp3  24530  metustto  24543  cfilucfil  24549  uniioombllem3  25577  dyadmbllem  25591  mbfconstlem  25619  i1fima2  25671  itg2gt0  25752  ellimc3  25871  limcflf  25873  limcresi  25877  limciun  25886  lhop  26008  ig1peu  26165  ig1pdvds  26170  psercnlem2  26414  dvloglem  26637  efopn  26647  noetalem1  27730  madess  27883  oldss  27887  cofcut1  27937  negsproplem2  28046  bdayons  28293  fnpreimac  32769  fsuppinisegfi  32786  gsumpart  33151  elrgspnsubrunlem2  33336  txomap  34025  zarcmplem  34072  tpr2rico  34103  pthhashvtx  35363  cvmsss2  35509  cvmopnlem  35513  cvmliftmolem1  35516  cvmliftlem15  35533  cvmlift2lem9  35546  imadifss  37969  poimirlem1  37995  poimirlem2  37996  poimirlem3  37997  poimirlem15  38009  poimirlem30  38024  dvtan  38044  heibor1lem  38183  aks6d1c2  42622  aks6d1c6lem3  42664  aks6d1c6lem5  42669  isnumbasabl  43558  isnumbasgrp  43559  dfacbasgrp  43560  trclimalb2  44177  frege81d  44198  imass2d  45712  limccog  46072  liminfgord  46204  uhgrimisgrgriclem  48428  clnbgrgrim  48432