Theorem imass2 5718

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

Syntax hints:   → wi 4   ⊆ wss 3769  ran crn 5313   ↾ cres 5314   “ cima 5315

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2377  ax-ext 2777

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2786  df-cleq 2792  df-clel 2795  df-nfc 2930  df-rab 3098  df-v 3387  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4116  df-if 4278  df-sn 4369  df-pr 4371  df-op 4375  df-br 4844  df-opab 4906  df-xp 5318  df-cnv 5320  df-dm 5322  df-rn 5323  df-res 5324  df-ima 5325

This theorem is referenced by:  funimass1  6182  funimass2  6183  fvimacnv  6558  f1imass  6749  ecinxp  8060  sbthlem1  8312  sbthlem2  8313  php3  8388  ordtypelem2  8666  tcrank  8997  limsupgord  14544  isercoll  14739  isacs1i  16632  gsumzf1o  18628  dprdres  18743  dprd2da  18757  dmdprdsplit2lem  18760  lmhmlsp  19370  f1lindf  20486  iscnp4  21396  cnpco  21400  cncls2i  21403  cnntri  21404  cnrest2  21419  cnpresti  21421  cnprest  21422  1stcfb  21577  xkococnlem  21791  qtopval2  21828  tgqtop  21844  qtoprest  21849  kqdisj  21864  regr1lem  21871  kqreglem1  21873  kqreglem2  21874  kqnrmlem1  21875  kqnrmlem2  21876  nrmhmph  21926  fbasrn  22016  elfm2  22080  fmfnfmlem1  22086  fmco  22093  flffbas  22127  cnpflf2  22132  cnextcn  22199  metcnp3  22673  metustto  22686  cfilucfil  22692  uniioombllem3  23693  dyadmbllem  23707  mbfconstlem  23735  i1fima2  23787  itg2gt0  23868  ellimc3  23984  limcflf  23986  limcresi  23990  limciun  23999  lhop  24120  ig1peu  24272  ig1pdvds  24277  psercnlem2  24519  dvloglem  24735  efopn  24745  txomap  30417  tpr2rico  30474  cvmsss2  31773  cvmopnlem  31777  cvmliftmolem1  31780  cvmliftlem15  31797  cvmlift2lem9  31810  imadifss  33873  poimirlem1  33899  poimirlem2  33900  poimirlem3  33901  poimirlem15  33913  poimirlem30  33928  dvtan  33948  heibor1lem  34095  isnumbasabl  38457  isnumbasgrp  38458  dfacbasgrp  38459  trclimalb2  38797  frege81d  38818  fnfvimad  40203  fnfvima2  40221  imass2d  40223  limccog  40592  liminfgord  40726