Theorem imass2 5999

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

Syntax hints:   → wi 4   ⊆ wss 3883  ran crn 5581   ↾ cres 5582   “ cima 5583

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071  df-opab 5133  df-xp 5586  df-cnv 5588  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593

This theorem is referenced by:  funimass1  6500  funimass2  6501  fvimacnv  6912  fnfvimad  7092  f1imass  7118  ecinxp  8539  sbthlem1  8823  sbthlem2  8824  php3  8899  ordtypelem2  9208  tcrank  9573  limsupgord  15109  isercoll  15307  isacs1i  17283  gsumzf1o  19428  dprdres  19546  dprd2da  19560  dmdprdsplit2lem  19563  lmhmlsp  20226  f1lindf  20939  iscnp4  22322  cnpco  22326  cncls2i  22329  cnntri  22330  cnrest2  22345  cnpresti  22347  cnprest  22348  1stcfb  22504  xkococnlem  22718  qtopval2  22755  tgqtop  22771  qtoprest  22776  kqdisj  22791  regr1lem  22798  kqreglem1  22800  kqreglem2  22801  kqnrmlem1  22802  kqnrmlem2  22803  nrmhmph  22853  fbasrn  22943  elfm2  23007  fmfnfmlem1  23013  fmco  23020  flffbas  23054  cnpflf2  23059  cnextcn  23126  metcnp3  23602  metustto  23615  cfilucfil  23621  uniioombllem3  24654  dyadmbllem  24668  mbfconstlem  24696  i1fima2  24748  itg2gt0  24830  ellimc3  24948  limcflf  24950  limcresi  24954  limciun  24963  lhop  25085  ig1peu  25241  ig1pdvds  25246  psercnlem2  25488  dvloglem  25708  efopn  25718  fnpreimac  30910  fsuppinisegfi  30923  gsumpart  31217  txomap  31686  zarcmplem  31733  tpr2rico  31764  pthhashvtx  32989  cvmsss2  33136  cvmopnlem  33140  cvmliftmolem1  33143  cvmliftlem15  33160  cvmlift2lem9  33173  noetalem1  33871  madess  33986  cofcut1  34017  imadifss  35679  poimirlem1  35705  poimirlem2  35706  poimirlem3  35707  poimirlem15  35719  poimirlem30  35734  dvtan  35754  heibor1lem  35894  isnumbasabl  40847  isnumbasgrp  40848  dfacbasgrp  40849  trclimalb2  41223  frege81d  41244  imass2d  42698  limccog  43051  liminfgord  43185