Theorem imass2 6067

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

Syntax hints:   → wi 4   ⊆ wss 3889  ran crn 5632   ↾ cres 5633   “ cima 5634

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086  df-opab 5148  df-xp 5637  df-cnv 5639  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644

This theorem is referenced by:  funimass1  6580  funimass2  6581  fvimacnv  7005  fnfvimad  7189  f1imass  7219  ecinxp  8739  sbthlem1  9025  sbthlem2  9026  php3  9143  ordtypelem2  9434  tcrank  9808  limsupgord  15434  isercoll  15630  isacs1i  17623  gsumzf1o  19887  dprdres  20005  dprd2da  20019  dmdprdsplit2lem  20022  lmhmlsp  21044  f1lindf  21802  iscnp4  23228  cnpco  23232  cncls2i  23235  cnntri  23236  cnrest2  23251  cnpresti  23253  cnprest  23254  1stcfb  23410  xkococnlem  23624  qtopval2  23661  tgqtop  23677  qtoprest  23682  kqdisj  23697  regr1lem  23704  kqreglem1  23706  kqreglem2  23707  kqnrmlem1  23708  kqnrmlem2  23709  nrmhmph  23759  fbasrn  23849  elfm2  23913  fmfnfmlem1  23919  fmco  23926  flffbas  23960  cnpflf2  23965  cnextcn  24032  metcnp3  24505  metustto  24518  cfilucfil  24524  uniioombllem3  25552  dyadmbllem  25566  mbfconstlem  25594  i1fima2  25646  itg2gt0  25727  ellimc3  25846  limcflf  25848  limcresi  25852  limciun  25861  lhop  25983  ig1peu  26140  ig1pdvds  26145  psercnlem2  26389  dvloglem  26612  efopn  26622  noetalem1  27705  madess  27858  oldss  27862  cofcut1  27912  negsproplem2  28021  bdayons  28268  fnpreimac  32743  fsuppinisegfi  32760  gsumpart  33124  elrgspnsubrunlem2  33309  txomap  33978  zarcmplem  34025  tpr2rico  34056  pthhashvtx  35310  cvmsss2  35456  cvmopnlem  35460  cvmliftmolem1  35463  cvmliftlem15  35480  cvmlift2lem9  35493  imadifss  37916  poimirlem1  37942  poimirlem2  37943  poimirlem3  37944  poimirlem15  37956  poimirlem30  37971  dvtan  37991  heibor1lem  38130  aks6d1c2  42569  aks6d1c6lem3  42611  aks6d1c6lem5  42616  isnumbasabl  43534  isnumbasgrp  43535  dfacbasgrp  43536  trclimalb2  44153  frege81d  44174  imass2d  45690  limccog  46050  liminfgord  46182  uhgrimisgrgriclem  48406  clnbgrgrim  48410