Theorem imass2 6028

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

Syntax hints:   → wi 4   ⊆ wss 3897  ran crn 5609   ↾ cres 5610   “ cima 5611

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2708

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2715  df-cleq 2729  df-clel 2815  df-rab 3405  df-v 3443  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4268  df-if 4472  df-sn 4572  df-pr 4574  df-op 4578  df-br 5088  df-opab 5150  df-xp 5614  df-cnv 5616  df-dm 5618  df-rn 5619  df-res 5620  df-ima 5621

This theorem is referenced by:  funimass1  6553  funimass2  6554  fvimacnv  6970  fnfvimad  7150  f1imass  7177  ecinxp  8631  sbthlem1  8927  sbthlem2  8928  php3  9056  php3OLD  9068  ordtypelem2  9355  tcrank  9720  limsupgord  15260  isercoll  15458  isacs1i  17443  gsumzf1o  19588  dprdres  19706  dprd2da  19720  dmdprdsplit2lem  19723  lmhmlsp  20394  f1lindf  21112  iscnp4  22497  cnpco  22501  cncls2i  22504  cnntri  22505  cnrest2  22520  cnpresti  22522  cnprest  22523  1stcfb  22679  xkococnlem  22893  qtopval2  22930  tgqtop  22946  qtoprest  22951  kqdisj  22966  regr1lem  22973  kqreglem1  22975  kqreglem2  22976  kqnrmlem1  22977  kqnrmlem2  22978  nrmhmph  23028  fbasrn  23118  elfm2  23182  fmfnfmlem1  23188  fmco  23195  flffbas  23229  cnpflf2  23234  cnextcn  23301  metcnp3  23779  metustto  23792  cfilucfil  23798  uniioombllem3  24832  dyadmbllem  24846  mbfconstlem  24874  i1fima2  24926  itg2gt0  25008  ellimc3  25126  limcflf  25128  limcresi  25132  limciun  25141  lhop  25263  ig1peu  25419  ig1pdvds  25424  psercnlem2  25666  dvloglem  25886  efopn  25896  fnpreimac  31143  fsuppinisegfi  31156  gsumpart  31450  txomap  31924  zarcmplem  31971  tpr2rico  32002  pthhashvtx  33228  cvmsss2  33375  cvmopnlem  33379  cvmliftmolem1  33382  cvmliftlem15  33399  cvmlift2lem9  33412  noetalem1  34018  madess  34133  cofcut1  34164  imadifss  35824  poimirlem1  35850  poimirlem2  35851  poimirlem3  35852  poimirlem15  35864  poimirlem30  35879  dvtan  35899  heibor1lem  36039  isnumbasabl  41148  isnumbasgrp  41149  dfacbasgrp  41150  trclimalb2  41568  frege81d  41589  imass2d  43051  limccog  43411  liminfgord  43545