Theorem imass2 6048

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

Syntax hints:   → wi 4   ⊆ wss 3900  ran crn 5615   ↾ cres 5616   “ cima 5617

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3394  df-v 3436  df-dif 3903  df-un 3905  df-in 3907  df-ss 3917  df-nul 4282  df-if 4474  df-sn 4575  df-pr 4577  df-op 4581  df-br 5090  df-opab 5152  df-xp 5620  df-cnv 5622  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627

This theorem is referenced by:  funimass1  6559  funimass2  6560  fvimacnv  6981  fnfvimad  7163  f1imass  7193  ecinxp  8711  sbthlem1  8995  sbthlem2  8996  php3  9113  ordtypelem2  9400  tcrank  9769  limsupgord  15371  isercoll  15567  isacs1i  17555  gsumzf1o  19817  dprdres  19935  dprd2da  19949  dmdprdsplit2lem  19952  lmhmlsp  20976  f1lindf  21752  iscnp4  23171  cnpco  23175  cncls2i  23178  cnntri  23179  cnrest2  23194  cnpresti  23196  cnprest  23197  1stcfb  23353  xkococnlem  23567  qtopval2  23604  tgqtop  23620  qtoprest  23625  kqdisj  23640  regr1lem  23647  kqreglem1  23649  kqreglem2  23650  kqnrmlem1  23651  kqnrmlem2  23652  nrmhmph  23702  fbasrn  23792  elfm2  23856  fmfnfmlem1  23862  fmco  23869  flffbas  23903  cnpflf2  23908  cnextcn  23975  metcnp3  24448  metustto  24461  cfilucfil  24467  uniioombllem3  25506  dyadmbllem  25520  mbfconstlem  25548  i1fima2  25600  itg2gt0  25681  ellimc3  25800  limcflf  25802  limcresi  25806  limciun  25815  lhop  25941  ig1peu  26100  ig1pdvds  26105  psercnlem2  26354  dvloglem  26577  efopn  26587  noetalem1  27673  madess  27814  oldss  27816  cofcut1  27857  negsproplem2  27964  bdayon  28202  fnpreimac  32643  fsuppinisegfi  32658  gsumpart  33027  elrgspnsubrunlem2  33205  txomap  33837  zarcmplem  33884  tpr2rico  33915  pthhashvtx  35140  cvmsss2  35286  cvmopnlem  35290  cvmliftmolem1  35293  cvmliftlem15  35310  cvmlift2lem9  35323  imadifss  37614  poimirlem1  37640  poimirlem2  37641  poimirlem3  37642  poimirlem15  37654  poimirlem30  37669  dvtan  37689  heibor1lem  37828  aks6d1c2  42142  aks6d1c6lem3  42184  aks6d1c6lem5  42189  isnumbasabl  43118  isnumbasgrp  43119  dfacbasgrp  43120  trclimalb2  43738  frege81d  43759  imass2d  45277  limccog  45639  liminfgord  45771  uhgrimisgrgriclem  47940  clnbgrgrim  47944