Theorem imass2 6095

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

Syntax hints:   → wi 4   ⊆ wss 3907  ran crn 5653   ↾ cres 5654   “ cima 5655

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-br 5106  df-opab 5168  df-xp 5658  df-cnv 5660  df-dm 5662  df-rn 5663  df-res 5664  df-ima 5665

This theorem is referenced by:  funimass1  6607  funimass2  6608  fvimacnv  7038  fnfvimad  7222  f1imass  7252  ecinxp  8778  sbthlem1  9063  sbthlem2  9064  php3  9181  ordtypelem2  9469  tcrank  9844  limsupgord  15513  isercoll  15709  isacs1i  17703  gsumzf1o  19973  dprdres  20091  dprd2da  20105  dmdprdsplit2lem  20108  lmhmlsp  21139  f1lindf  21932  iscnp4  23381  cnpco  23385  cncls2i  23388  cnntri  23389  cnrest2  23404  cnpresti  23406  cnprest  23407  1stcfb  23563  xkococnlem  23777  qtopval2  23814  tgqtop  23830  qtoprest  23835  kqdisj  23850  regr1lem  23857  kqreglem1  23859  kqreglem2  23860  kqnrmlem1  23861  kqnrmlem2  23862  nrmhmph  23912  fbasrn  24002  elfm2  24066  fmfnfmlem1  24072  fmco  24079  flffbas  24113  cnpflf2  24118  cnextcn  24185  metcnp3  24658  metustto  24671  cfilucfil  24677  uniioombllem3  25705  dyadmbllem  25719  mbfconstlem  25747  i1fima2  25799  itg2gt0  25880  ellimc3  25999  limcflf  26001  limcresi  26005  limciun  26014  lhop  26136  ig1peu  26293  ig1pdvds  26298  psercnlem2  26545  dvloglem  26771  efopn  26781  noetalem1  27863  madess  28017  oldss  28021  cofcut1  28071  negsproplem2  28180  bdayons  28427  fnpreimac  32927  fsuppinisegfi  32944  gsumpart  33296  elrgspnsubrunlem2  33481  txomap  34141  zarcmplem  34188  tpr2rico  34219  pthhashvtx  35491  cvmsss2  35637  cvmopnlem  35641  cvmliftmolem1  35644  cvmliftlem15  35661  cvmlift2lem9  35674  imadifss  38106  poimirlem1  38132  poimirlem2  38133  poimirlem3  38134  poimirlem15  38146  poimirlem30  38161  dvtan  38181  heibor1lem  38320  aks6d1c2  42759  aks6d1c6lem3  42801  aks6d1c6lem5  42806  isnumbasabl  43695  isnumbasgrp  43696  dfacbasgrp  43697  trclimalb2  44314  frege81d  44335  imass2d  45834  limccog  46194  liminfgord  46326  uhgrimisgrgriclem  48550  clnbgrgrim  48554