Theorem imass2 5755

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

Syntax hints:   → wi 4   ⊆ wss 3792  ran crn 5356   ↾ cres 5357   “ cima 5358

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-rab 3099  df-v 3400  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-sn 4399  df-pr 4401  df-op 4405  df-br 4887  df-opab 4949  df-xp 5361  df-cnv 5363  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368

This theorem is referenced by:  funimass1  6216  funimass2  6217  fvimacnv  6595  fnfvimad  6766  f1imass  6793  ecinxp  8105  sbthlem1  8358  sbthlem2  8359  php3  8434  ordtypelem2  8713  tcrank  9044  limsupgord  14611  isercoll  14806  isacs1i  16703  gsumzf1o  18699  dprdres  18814  dprd2da  18828  dmdprdsplit2lem  18831  lmhmlsp  19444  f1lindf  20565  iscnp4  21475  cnpco  21479  cncls2i  21482  cnntri  21483  cnrest2  21498  cnpresti  21500  cnprest  21501  1stcfb  21657  xkococnlem  21871  qtopval2  21908  tgqtop  21924  qtoprest  21929  kqdisj  21944  regr1lem  21951  kqreglem1  21953  kqreglem2  21954  kqnrmlem1  21955  kqnrmlem2  21956  nrmhmph  22006  fbasrn  22096  elfm2  22160  fmfnfmlem1  22166  fmco  22173  flffbas  22207  cnpflf2  22212  cnextcn  22279  metcnp3  22753  metustto  22766  cfilucfil  22772  uniioombllem3  23789  dyadmbllem  23803  mbfconstlem  23831  i1fima2  23883  itg2gt0  23964  ellimc3  24080  limcflf  24082  limcresi  24086  limciun  24095  lhop  24216  ig1peu  24368  ig1pdvds  24373  psercnlem2  24615  dvloglem  24831  efopn  24841  fnpreimac  30036  txomap  30499  tpr2rico  30556  cvmsss2  31855  cvmopnlem  31859  cvmliftmolem1  31862  cvmliftlem15  31879  cvmlift2lem9  31892  imadifss  34011  poimirlem1  34038  poimirlem2  34039  poimirlem3  34040  poimirlem15  34052  poimirlem30  34067  dvtan  34087  heibor1lem  34234  isnumbasabl  38639  isnumbasgrp  38640  dfacbasgrp  38641  trclimalb2  38979  frege81d  39000  fnfvima2  40393  imass2d  40395  limccog  40764  liminfgord  40898