Theorem imass2 6010

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

Syntax hints:   → wi 4   ⊆ wss 3887  ran crn 5590   ↾ cres 5591   “ cima 5592

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-br 5075  df-opab 5137  df-xp 5595  df-cnv 5597  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602

This theorem is referenced by:  funimass1  6516  funimass2  6517  fvimacnv  6930  fnfvimad  7110  f1imass  7137  ecinxp  8581  sbthlem1  8870  sbthlem2  8871  php3  8995  php3OLD  9007  ordtypelem2  9278  tcrank  9642  limsupgord  15181  isercoll  15379  isacs1i  17366  gsumzf1o  19513  dprdres  19631  dprd2da  19645  dmdprdsplit2lem  19648  lmhmlsp  20311  f1lindf  21029  iscnp4  22414  cnpco  22418  cncls2i  22421  cnntri  22422  cnrest2  22437  cnpresti  22439  cnprest  22440  1stcfb  22596  xkococnlem  22810  qtopval2  22847  tgqtop  22863  qtoprest  22868  kqdisj  22883  regr1lem  22890  kqreglem1  22892  kqreglem2  22893  kqnrmlem1  22894  kqnrmlem2  22895  nrmhmph  22945  fbasrn  23035  elfm2  23099  fmfnfmlem1  23105  fmco  23112  flffbas  23146  cnpflf2  23151  cnextcn  23218  metcnp3  23696  metustto  23709  cfilucfil  23715  uniioombllem3  24749  dyadmbllem  24763  mbfconstlem  24791  i1fima2  24843  itg2gt0  24925  ellimc3  25043  limcflf  25045  limcresi  25049  limciun  25058  lhop  25180  ig1peu  25336  ig1pdvds  25341  psercnlem2  25583  dvloglem  25803  efopn  25813  fnpreimac  31008  fsuppinisegfi  31021  gsumpart  31315  txomap  31784  zarcmplem  31831  tpr2rico  31862  pthhashvtx  33089  cvmsss2  33236  cvmopnlem  33240  cvmliftmolem1  33243  cvmliftlem15  33260  cvmlift2lem9  33273  noetalem1  33944  madess  34059  cofcut1  34090  imadifss  35752  poimirlem1  35778  poimirlem2  35779  poimirlem3  35780  poimirlem15  35792  poimirlem30  35807  dvtan  35827  heibor1lem  35967  isnumbasabl  40931  isnumbasgrp  40932  dfacbasgrp  40933  trclimalb2  41334  frege81d  41355  imass2d  42809  limccog  43161  liminfgord  43295