Theorem imass2 6073

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

Syntax hints:   → wi 4   ⊆ wss 3914  ran crn 5639   ↾ cres 5640   “ cima 5641

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-opab 5170  df-xp 5644  df-cnv 5646  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651

This theorem is referenced by:  funimass1  6598  funimass2  6599  fvimacnv  7025  fnfvimad  7208  f1imass  7239  ecinxp  8765  sbthlem1  9051  sbthlem2  9052  php3  9173  ordtypelem2  9472  tcrank  9837  limsupgord  15438  isercoll  15634  isacs1i  17618  gsumzf1o  19842  dprdres  19960  dprd2da  19974  dmdprdsplit2lem  19977  lmhmlsp  20956  f1lindf  21731  iscnp4  23150  cnpco  23154  cncls2i  23157  cnntri  23158  cnrest2  23173  cnpresti  23175  cnprest  23176  1stcfb  23332  xkococnlem  23546  qtopval2  23583  tgqtop  23599  qtoprest  23604  kqdisj  23619  regr1lem  23626  kqreglem1  23628  kqreglem2  23629  kqnrmlem1  23630  kqnrmlem2  23631  nrmhmph  23681  fbasrn  23771  elfm2  23835  fmfnfmlem1  23841  fmco  23848  flffbas  23882  cnpflf2  23887  cnextcn  23954  metcnp3  24428  metustto  24441  cfilucfil  24447  uniioombllem3  25486  dyadmbllem  25500  mbfconstlem  25528  i1fima2  25580  itg2gt0  25661  ellimc3  25780  limcflf  25782  limcresi  25786  limciun  25795  lhop  25921  ig1peu  26080  ig1pdvds  26085  psercnlem2  26334  dvloglem  26557  efopn  26567  noetalem1  27653  madess  27788  cofcut1  27828  negsproplem2  27935  bdayon  28173  fnpreimac  32595  fsuppinisegfi  32610  gsumpart  32997  elrgspnsubrunlem2  33199  txomap  33824  zarcmplem  33871  tpr2rico  33902  pthhashvtx  35115  cvmsss2  35261  cvmopnlem  35265  cvmliftmolem1  35268  cvmliftlem15  35285  cvmlift2lem9  35298  imadifss  37589  poimirlem1  37615  poimirlem2  37616  poimirlem3  37617  poimirlem15  37629  poimirlem30  37644  dvtan  37664  heibor1lem  37803  aks6d1c2  42118  aks6d1c6lem3  42160  aks6d1c6lem5  42165  isnumbasabl  43095  isnumbasgrp  43096  dfacbasgrp  43097  trclimalb2  43715  frege81d  43736  imass2d  45255  limccog  45618  liminfgord  45752  uhgrimisgrgriclem  47930  clnbgrgrim  47934