Theorem imass2 6059

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

Syntax hints:   → wi 4   ⊆ wss 3913  ran crn 5639   ↾ cres 5640   “ cima 5641

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3406  df-v 3448  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-br 5111  df-opab 5173  df-xp 5644  df-cnv 5646  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651

This theorem is referenced by:  funimass1  6588  funimass2  6589  fvimacnv  7008  fnfvimad  7189  f1imass  7216  ecinxp  8738  sbthlem1  9034  sbthlem2  9035  php3  9163  php3OLD  9175  ordtypelem2  9464  tcrank  9829  limsupgord  15366  isercoll  15564  isacs1i  17551  gsumzf1o  19703  dprdres  19821  dprd2da  19835  dmdprdsplit2lem  19838  lmhmlsp  20567  f1lindf  21265  iscnp4  22651  cnpco  22655  cncls2i  22658  cnntri  22659  cnrest2  22674  cnpresti  22676  cnprest  22677  1stcfb  22833  xkococnlem  23047  qtopval2  23084  tgqtop  23100  qtoprest  23105  kqdisj  23120  regr1lem  23127  kqreglem1  23129  kqreglem2  23130  kqnrmlem1  23131  kqnrmlem2  23132  nrmhmph  23182  fbasrn  23272  elfm2  23336  fmfnfmlem1  23342  fmco  23349  flffbas  23383  cnpflf2  23388  cnextcn  23455  metcnp3  23933  metustto  23946  cfilucfil  23952  uniioombllem3  24986  dyadmbllem  25000  mbfconstlem  25028  i1fima2  25080  itg2gt0  25162  ellimc3  25280  limcflf  25282  limcresi  25286  limciun  25295  lhop  25417  ig1peu  25573  ig1pdvds  25578  psercnlem2  25820  dvloglem  26040  efopn  26050  noetalem1  27126  madess  27249  cofcut1  27282  negsproplem2  27370  fnpreimac  31654  fsuppinisegfi  31669  gsumpart  31967  txomap  32504  zarcmplem  32551  tpr2rico  32582  pthhashvtx  33808  cvmsss2  33955  cvmopnlem  33959  cvmliftmolem1  33962  cvmliftlem15  33979  cvmlift2lem9  33992  imadifss  36126  poimirlem1  36152  poimirlem2  36153  poimirlem3  36154  poimirlem15  36166  poimirlem30  36181  dvtan  36201  heibor1lem  36341  isnumbasabl  41491  isnumbasgrp  41492  dfacbasgrp  41493  trclimalb2  42120  frege81d  42141  imass2d  43611  limccog  43981  liminfgord  44115