Theorem imass2 6120

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

Syntax hints:   → wi 4   ⊆ wss 3951  ran crn 5686   ↾ cres 5687   “ cima 5688

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-opab 5206  df-xp 5691  df-cnv 5693  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698

This theorem is referenced by:  funimass1  6648  funimass2  6649  fvimacnv  7073  fnfvimad  7254  f1imass  7284  ecinxp  8832  sbthlem1  9123  sbthlem2  9124  php3  9249  php3OLD  9261  ordtypelem2  9559  tcrank  9924  limsupgord  15508  isercoll  15704  isacs1i  17700  gsumzf1o  19930  dprdres  20048  dprd2da  20062  dmdprdsplit2lem  20065  lmhmlsp  21048  f1lindf  21842  iscnp4  23271  cnpco  23275  cncls2i  23278  cnntri  23279  cnrest2  23294  cnpresti  23296  cnprest  23297  1stcfb  23453  xkococnlem  23667  qtopval2  23704  tgqtop  23720  qtoprest  23725  kqdisj  23740  regr1lem  23747  kqreglem1  23749  kqreglem2  23750  kqnrmlem1  23751  kqnrmlem2  23752  nrmhmph  23802  fbasrn  23892  elfm2  23956  fmfnfmlem1  23962  fmco  23969  flffbas  24003  cnpflf2  24008  cnextcn  24075  metcnp3  24553  metustto  24566  cfilucfil  24572  uniioombllem3  25620  dyadmbllem  25634  mbfconstlem  25662  i1fima2  25714  itg2gt0  25795  ellimc3  25914  limcflf  25916  limcresi  25920  limciun  25929  lhop  26055  ig1peu  26214  ig1pdvds  26219  psercnlem2  26468  dvloglem  26690  efopn  26700  noetalem1  27786  madess  27915  cofcut1  27954  negsproplem2  28061  fnpreimac  32681  fsuppinisegfi  32696  gsumpart  33060  elrgspnsubrunlem2  33252  txomap  33833  zarcmplem  33880  tpr2rico  33911  pthhashvtx  35133  cvmsss2  35279  cvmopnlem  35283  cvmliftmolem1  35286  cvmliftlem15  35303  cvmlift2lem9  35316  imadifss  37602  poimirlem1  37628  poimirlem2  37629  poimirlem3  37630  poimirlem15  37642  poimirlem30  37657  dvtan  37677  heibor1lem  37816  aks6d1c2  42131  aks6d1c6lem3  42173  aks6d1c6lem5  42178  isnumbasabl  43118  isnumbasgrp  43119  dfacbasgrp  43120  trclimalb2  43739  frege81d  43760  imass2d  45268  limccog  45635  liminfgord  45769  uhgrimisgrgriclem  47898  clnbgrgrim  47902