Theorem imass2 6061

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

Syntax hints:   → wi 4   ⊆ wss 3901  ran crn 5625   ↾ cres 5626   “ cima 5627

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 2115  ax-9 2123  ax-ext 2708

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 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099  df-opab 5161  df-xp 5630  df-cnv 5632  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637

This theorem is referenced by:  funimass1  6574  funimass2  6575  fvimacnv  6998  fnfvimad  7180  f1imass  7210  ecinxp  8729  sbthlem1  9015  sbthlem2  9016  php3  9133  ordtypelem2  9424  tcrank  9796  limsupgord  15395  isercoll  15591  isacs1i  17580  gsumzf1o  19841  dprdres  19959  dprd2da  19973  dmdprdsplit2lem  19976  lmhmlsp  21001  f1lindf  21777  iscnp4  23207  cnpco  23211  cncls2i  23214  cnntri  23215  cnrest2  23230  cnpresti  23232  cnprest  23233  1stcfb  23389  xkococnlem  23603  qtopval2  23640  tgqtop  23656  qtoprest  23661  kqdisj  23676  regr1lem  23683  kqreglem1  23685  kqreglem2  23686  kqnrmlem1  23687  kqnrmlem2  23688  nrmhmph  23738  fbasrn  23828  elfm2  23892  fmfnfmlem1  23898  fmco  23905  flffbas  23939  cnpflf2  23944  cnextcn  24011  metcnp3  24484  metustto  24497  cfilucfil  24503  uniioombllem3  25542  dyadmbllem  25556  mbfconstlem  25584  i1fima2  25636  itg2gt0  25717  ellimc3  25836  limcflf  25838  limcresi  25842  limciun  25851  lhop  25977  ig1peu  26136  ig1pdvds  26141  psercnlem2  26390  dvloglem  26613  efopn  26623  noetalem1  27709  madess  27862  oldss  27866  cofcut1  27916  negsproplem2  28025  bdayons  28272  fnpreimac  32749  fsuppinisegfi  32766  gsumpart  33146  elrgspnsubrunlem2  33330  txomap  33991  zarcmplem  34038  tpr2rico  34069  pthhashvtx  35322  cvmsss2  35468  cvmopnlem  35472  cvmliftmolem1  35475  cvmliftlem15  35492  cvmlift2lem9  35505  imadifss  37792  poimirlem1  37818  poimirlem2  37819  poimirlem3  37820  poimirlem15  37832  poimirlem30  37847  dvtan  37867  heibor1lem  38006  aks6d1c2  42380  aks6d1c6lem3  42422  aks6d1c6lem5  42427  isnumbasabl  43344  isnumbasgrp  43345  dfacbasgrp  43346  trclimalb2  43963  frege81d  43984  imass2d  45501  limccog  45862  liminfgord  45994  uhgrimisgrgriclem  48172  clnbgrgrim  48176