Theorem imass2 6069

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

Syntax hints:   → wi 4   ⊆ wss 3903  ran crn 5633   ↾ cres 5634   “ cima 5635

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-xp 5638  df-cnv 5640  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645

This theorem is referenced by:  funimass1  6582  funimass2  6583  fvimacnv  7007  fnfvimad  7190  f1imass  7220  ecinxp  8741  sbthlem1  9027  sbthlem2  9028  php3  9145  ordtypelem2  9436  tcrank  9808  limsupgord  15407  isercoll  15603  isacs1i  17592  gsumzf1o  19853  dprdres  19971  dprd2da  19985  dmdprdsplit2lem  19988  lmhmlsp  21013  f1lindf  21789  iscnp4  23219  cnpco  23223  cncls2i  23226  cnntri  23227  cnrest2  23242  cnpresti  23244  cnprest  23245  1stcfb  23401  xkococnlem  23615  qtopval2  23652  tgqtop  23668  qtoprest  23673  kqdisj  23688  regr1lem  23695  kqreglem1  23697  kqreglem2  23698  kqnrmlem1  23699  kqnrmlem2  23700  nrmhmph  23750  fbasrn  23840  elfm2  23904  fmfnfmlem1  23910  fmco  23917  flffbas  23951  cnpflf2  23956  cnextcn  24023  metcnp3  24496  metustto  24509  cfilucfil  24515  uniioombllem3  25554  dyadmbllem  25568  mbfconstlem  25596  i1fima2  25648  itg2gt0  25729  ellimc3  25848  limcflf  25850  limcresi  25854  limciun  25863  lhop  25989  ig1peu  26148  ig1pdvds  26153  psercnlem2  26402  dvloglem  26625  efopn  26635  noetalem1  27721  madess  27874  oldss  27878  cofcut1  27928  negsproplem2  28037  bdayons  28284  fnpreimac  32759  fsuppinisegfi  32776  gsumpart  33156  elrgspnsubrunlem2  33341  txomap  34011  zarcmplem  34058  tpr2rico  34089  pthhashvtx  35341  cvmsss2  35487  cvmopnlem  35491  cvmliftmolem1  35494  cvmliftlem15  35511  cvmlift2lem9  35524  imadifss  37840  poimirlem1  37866  poimirlem2  37867  poimirlem3  37868  poimirlem15  37880  poimirlem30  37895  dvtan  37915  heibor1lem  38054  aks6d1c2  42494  aks6d1c6lem3  42536  aks6d1c6lem5  42541  isnumbasabl  43457  isnumbasgrp  43458  dfacbasgrp  43459  trclimalb2  44076  frege81d  44097  imass2d  45613  limccog  45974  liminfgord  46106  uhgrimisgrgriclem  48284  clnbgrgrim  48288