Theorem fssres 6774

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 6566	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
2		fnssres 6691	. . . . 5 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶) Fn 𝐶)
3		resss 6021	. . . . . . 7 ⊢ (𝐹 ↾ 𝐶) ⊆ 𝐹
4	3	rnssi 5953	. . . . . 6 ⊢ ran (𝐹 ↾ 𝐶) ⊆ ran 𝐹
5		sstr 4003	. . . . . 6 ⊢ ((ran (𝐹 ↾ 𝐶) ⊆ ran 𝐹 ∧ ran 𝐹 ⊆ 𝐵) → ran (𝐹 ↾ 𝐶) ⊆ 𝐵)
6	4, 5	mpan 690	. . . . 5 ⊢ (ran 𝐹 ⊆ 𝐵 → ran (𝐹 ↾ 𝐶) ⊆ 𝐵)
7	2, 6	anim12i 613	. . . 4 ⊢ (((𝐹 Fn 𝐴 ∧ 𝐶 ⊆ 𝐴) ∧ ran 𝐹 ⊆ 𝐵) → ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵))
8	7	an32s 652	. . 3 ⊢ (((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) ∧ 𝐶 ⊆ 𝐴) → ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵))
9	1, 8	sylanb 581	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ⊆ 𝐴) → ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵))
10		df-f 6566	. 2 ⊢ ((𝐹 ↾ 𝐶):𝐶⟶𝐵 ↔ ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵))
11	9, 10	sylibr 234	1 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶):𝐶⟶𝐵)

Syntax hints:   → wi 4   ∧ wa 395   ⊆ wss 3962  ran crn 5689   ↾ cres 5690   Fn wfn 6557  ⟶wf 6558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5148  df-opab 5210  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-fun 6564  df-fn 6565  df-f 6566

This theorem is referenced by:  fssresd  6775  fssres2  6776  fresin  6777  fresaun  6779  f1ssres  6811  f2ndf  8143  elmapssres  8905  pmresg  8908  ralxpmap  8934  mapunen  9184  fofinf1o  9369  fseqenlem1  10061  inar1  10812  gruima  10839  addnqf  10985  mulnqf  10986  fseq1p1m1  13634  injresinj  13823  seqf1olem2  14079  wrdred1  14594  rlimres  15590  lo1res  15591  vdwnnlem1  17028  fsets  17202  resmgmhm  18736  resmhm  18845  resghm  19262  gsumzres  19941  gsumzadd  19954  gsum2dlem2  20003  dpjidcl  20092  ablfac1eu  20107  abvres  20848  znf1o  21587  islindf4  21875  kgencn  23579  ptrescn  23662  hmeores  23794  tsmsres  24167  tsmsmhm  24169  tsmsadd  24170  xrge0gsumle  24868  xrge0tsms  24869  ovolicc2lem4  25568  limcdif  25925  limcflf  25930  limcmo  25931  dvres  25960  dvres3a  25963  aannenlem1  26384  logcn  26703  dvlog  26707  dvlog2  26709  logtayl  26716  dvatan  26992  atancn  26993  efrlim  27026  efrlimOLD  27027  amgm  27048  dchrelbas2  27295  redwlklem  29703  pthdivtx  29761  hhssabloilem  31289  hhssnv  31292  wrdres  32903  gsumpart  33042  xrge0tsmsd  33047  cntmeas  34206  eulerpartlemt  34352  eulerpartlemmf  34356  eulerpartlemgvv  34357  subiwrd  34366  sseqp1  34376  poimirlem4  37610  mbfresfi  37652  mbfposadd  37653  itg2gt0cn  37661  sdclem2  37728  mzpcompact2lem  42738  eldiophb  42744  eldioph2  42749  cncfiooicclem1  45848  fouriersw  46186  sge0tsms  46335  psmeasure  46426  sssmf  46693  lindslinindimp2lem2  48304