Theorem imass2 6089

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

Syntax hints:   → wi 4   ⊆ wss 3926  ran crn 5655   ↾ cres 5656   “ cima 5657

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-br 5120  df-opab 5182  df-xp 5660  df-cnv 5662  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667

This theorem is referenced by:  funimass1  6617  funimass2  6618  fvimacnv  7042  fnfvimad  7225  f1imass  7256  ecinxp  8804  sbthlem1  9095  sbthlem2  9096  php3  9221  php3OLD  9231  ordtypelem2  9531  tcrank  9896  limsupgord  15486  isercoll  15682  isacs1i  17667  gsumzf1o  19891  dprdres  20009  dprd2da  20023  dmdprdsplit2lem  20026  lmhmlsp  21005  f1lindf  21780  iscnp4  23199  cnpco  23203  cncls2i  23206  cnntri  23207  cnrest2  23222  cnpresti  23224  cnprest  23225  1stcfb  23381  xkococnlem  23595  qtopval2  23632  tgqtop  23648  qtoprest  23653  kqdisj  23668  regr1lem  23675  kqreglem1  23677  kqreglem2  23678  kqnrmlem1  23679  kqnrmlem2  23680  nrmhmph  23730  fbasrn  23820  elfm2  23884  fmfnfmlem1  23890  fmco  23897  flffbas  23931  cnpflf2  23936  cnextcn  24003  metcnp3  24477  metustto  24490  cfilucfil  24496  uniioombllem3  25536  dyadmbllem  25550  mbfconstlem  25578  i1fima2  25630  itg2gt0  25711  ellimc3  25830  limcflf  25832  limcresi  25836  limciun  25845  lhop  25971  ig1peu  26130  ig1pdvds  26135  psercnlem2  26384  dvloglem  26607  efopn  26617  noetalem1  27703  madess  27832  cofcut1  27871  negsproplem2  27978  fnpreimac  32595  fsuppinisegfi  32610  gsumpart  32997  elrgspnsubrunlem2  33189  txomap  33811  zarcmplem  33858  tpr2rico  33889  pthhashvtx  35096  cvmsss2  35242  cvmopnlem  35246  cvmliftmolem1  35249  cvmliftlem15  35266  cvmlift2lem9  35279  imadifss  37565  poimirlem1  37591  poimirlem2  37592  poimirlem3  37593  poimirlem15  37605  poimirlem30  37620  dvtan  37640  heibor1lem  37779  aks6d1c2  42089  aks6d1c6lem3  42131  aks6d1c6lem5  42136  isnumbasabl  43077  isnumbasgrp  43078  dfacbasgrp  43079  trclimalb2  43697  frege81d  43718  imass2d  45233  limccog  45597  liminfgord  45731  uhgrimisgrgriclem  47891  clnbgrgrim  47895