Theorem fssres 6700

Description: Restriction of a function with a subclass of its domain. (Contributed by NM, 23-Sep-2004.)

Assertion

Ref	Expression
fssres	⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶):𝐶⟶𝐵)

Proof of Theorem fssres

Step	Hyp	Ref	Expression
1		df-f 6496	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
2		fnssres 6615	. . . . 5 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶) Fn 𝐶)
3		resss 5960	. . . . . . 7 ⊢ (𝐹 ↾ 𝐶) ⊆ 𝐹
4	3	rnssi 5889	. . . . . 6 ⊢ ran (𝐹 ↾ 𝐶) ⊆ ran 𝐹
5		sstr 3931	. . . . . 6 ⊢ ((ran (𝐹 ↾ 𝐶) ⊆ ran 𝐹 ∧ ran 𝐹 ⊆ 𝐵) → ran (𝐹 ↾ 𝐶) ⊆ 𝐵)
6	4, 5	mpan 691	. . . . 5 ⊢ (ran 𝐹 ⊆ 𝐵 → ran (𝐹 ↾ 𝐶) ⊆ 𝐵)
7	2, 6	anim12i 614	. . . 4 ⊢ (((𝐹 Fn 𝐴 ∧ 𝐶 ⊆ 𝐴) ∧ ran 𝐹 ⊆ 𝐵) → ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵))
8	7	an32s 653	. . 3 ⊢ (((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) ∧ 𝐶 ⊆ 𝐴) → ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵))
9	1, 8	sylanb 582	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ⊆ 𝐴) → ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵))
10		df-f 6496	. 2 ⊢ ((𝐹 ↾ 𝐶):𝐶⟶𝐵 ↔ ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵))
11	9, 10	sylibr 234	1 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶):𝐶⟶𝐵)

Syntax hints:   → wi 4   ∧ wa 395   ⊆ wss 3890  ran crn 5625   ↾ cres 5626   Fn wfn 6487  ⟶wf 6488

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 2709  ax-sep 5231  ax-pr 5370

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 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-fun 6494  df-fn 6495  df-f 6496

This theorem is referenced by:  fssresd  6701  fssres2  6702  fresin  6703  fresaun  6705  f1ssres  6737  resf1extb  7878  resf1ext2b  7879  f2ndf  8063  elmapssres  8807  pmresg  8811  ralxpmap  8837  mapunen  9077  fofinf1o  9235  fseqenlem1  9937  inar1  10689  gruima  10716  addnqf  10862  mulnqf  10863  fseq1p1m1  13543  injresinj  13737  seqf1olem2  13995  wrdred1  14513  rlimres  15511  lo1res  15512  vdwnnlem1  16957  fsets  17130  resmgmhm  18670  resmhm  18779  resghm  19198  gsumzres  19875  gsumzadd  19888  gsum2dlem2  19937  dpjidcl  20026  ablfac1eu  20041  abvres  20799  znf1o  21541  islindf4  21828  kgencn  23531  ptrescn  23614  hmeores  23746  tsmsres  24119  tsmsmhm  24121  tsmsadd  24122  xrge0gsumle  24809  xrge0tsms  24810  ovolicc2lem4  25497  limcdif  25853  limcflf  25858  limcmo  25859  dvres  25888  dvres3a  25891  aannenlem1  26305  logcn  26624  dvlog  26628  dvlog2  26630  logtayl  26637  dvatan  26912  atancn  26913  efrlim  26946  efrlimOLD  26947  amgm  26968  dchrelbas2  27214  redwlklem  29753  pthdivtx  29810  hhssabloilem  31347  hhssnv  31350  wrdres  33010  gsumpart  33139  xrge0tsmsd  33149  cntmeas  34386  eulerpartlemt  34531  eulerpartlemmf  34535  eulerpartlemgvv  34536  subiwrd  34545  sseqp1  34555  poimirlem4  37959  mbfresfi  38001  mbfposadd  38002  itg2gt0cn  38010  sdclem2  38077  mzpcompact2lem  43197  eldiophb  43203  eldioph2  43208  cncfiooicclem1  46339  fouriersw  46677  sge0tsms  46826  psmeasure  46917  sssmf  47184  lindslinindimp2lem2  48947