Theorem imass2 5420

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

Syntax hints:   → wi 4   ⊆ wss 3540  ran crn 5039   ↾ cres 5040   “ cima 5041

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4584  df-opab 4644  df-xp 5044  df-cnv 5046  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051

This theorem is referenced by:  funimass1  5885  funimass2  5886  fvimacnv  6240  f1imass  6422  ecinxp  7709  sbthlem1  7955  sbthlem2  7956  php3  8031  ordtypelem2  8307  tcrank  8630  limsupgord  14051  isercoll  14246  isacs1i  16141  gsumzf1o  18136  dprdres  18250  dprd2da  18264  dmdprdsplit2lem  18267  lmhmlsp  18870  f1lindf  19980  iscnp4  20877  cnpco  20881  cncls2i  20884  cnntri  20885  cnrest2  20900  cnpresti  20902  cnprest  20903  1stcfb  21058  xkococnlem  21272  qtopval2  21309  tgqtop  21325  qtoprest  21330  kqdisj  21345  regr1lem  21352  kqreglem1  21354  kqreglem2  21355  kqnrmlem1  21356  kqnrmlem2  21357  nrmhmph  21407  fbasrn  21498  elfm2  21562  fmfnfmlem1  21568  fmco  21575  flffbas  21609  cnpflf2  21614  cnextcn  21681  metcnp3  22155  metustto  22168  cfilucfil  22174  uniioombllem3  23159  dyadmbllem  23173  mbfconstlem  23202  i1fima2  23252  itg2gt0  23333  ellimc3  23449  limcflf  23451  limcresi  23455  limciun  23464  lhop  23583  ig1peu  23735  ig1pdvds  23740  psercnlem2  23982  dvloglem  24194  efopn  24204  txomap  29229  tpr2rico  29286  cvmsss2  30510  cvmopnlem  30514  cvmliftmolem1  30517  cvmliftlem15  30534  cvmlift2lem9  30547  nofulllem3  31103  imadifss  32554  poimirlem1  32580  poimirlem2  32581  poimirlem3  32582  poimirlem15  32594  poimirlem30  32609  dvtan  32630  heibor1lem  32778  isnumbasabl  36695  isnumbasgrp  36696  dfacbasgrp  36697  trclimalb2  37037  frege81d  37058  limccog  38687