Theorem funres 6582

Description: A restriction of a function is a function. Compare Exercise 18 of [TakeutiZaring] p. 25. (Contributed by NM, 16-Aug-1994.)

Assertion

Ref	Expression
funres	⊢ (Fun 𝐹 → Fun (𝐹 ↾ 𝐴))

Proof of Theorem funres

Step	Hyp	Ref	Expression
1		resss 6002	. 2 ⊢ (𝐹 ↾ 𝐴) ⊆ 𝐹
2		funss 6559	. 2 ⊢ ((𝐹 ↾ 𝐴) ⊆ 𝐹 → (Fun 𝐹 → Fun (𝐹 ↾ 𝐴)))
3	1, 2	ax-mp 5	1 ⊢ (Fun 𝐹 → Fun (𝐹 ↾ 𝐴))

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3906   ↾ cres 5665  Fun wfun 6534

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-in 3913  df-ss 3923  df-br 5112  df-opab 5176  df-rel 5670  df-cnv 5671  df-co 5672  df-res 5675  df-fun 6542

This theorem is used by:  funresd  6583  fores  6806  resfunexg  7217  funfvima  7232  funiunfv  7248  fprlem1  8299  smores  8341  smores2  8343  frfnom  8424  sbthlem7  9084  fsuppres  9356  ordtypelem4  9486  wdomima2g  9551  imadomg  10529  hashres  14489  hashimarn  14491  setsfun  17249  setsfun0  17250  lubfun  18424  glbfun  18437  qtoptop2  23887  volf  25719  nolesgn2ores  27867  nosupres  27902  nosupbnd2lem1  27910  noetasuplem4  27931  noetainflem4  27935  oniso  28495  bdayn0sf1o  28594  uhgrspansubgrlem  29674  upgrres  29690  umgrres  29691  hlimf  31636  fsuppcurry1  33115  fsuppcurry2  33116  eulerpartlemmf  34806  eulerpartlemgvv  34807  bj-funidres  37828  imadomfi  42802  funcoressn  47812  fundmdfat  47899  afvelrn  47938  dmfcoafv  47945  aovmpt4g  47971  fundmafv2rnb  48000