Theorem funres 6534

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 5960	. 2 ⊢ (𝐹 ↾ 𝐴) ⊆ 𝐹
2		funss 6511	. 2 ⊢ ((𝐹 ↾ 𝐴) ⊆ 𝐹 → (Fun 𝐹 → Fun (𝐹 ↾ 𝐴)))
3	1, 2	ax-mp 5	1 ⊢ (Fun 𝐹 → Fun (𝐹 ↾ 𝐴))

Syntax hints:   → wi 4   ⊆ wss 3901   ↾ cres 5626  Fun wfun 6486

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-in 3908  df-ss 3918  df-br 5099  df-opab 5161  df-rel 5631  df-cnv 5632  df-co 5633  df-res 5636  df-fun 6494

This theorem is referenced by:  funresd  6535  fores  6756  resfunexg  7161  funfvima  7176  funiunfv  7194  fprlem1  8242  smores  8284  smores2  8286  frfnom  8366  sbthlem7  9021  fsuppres  9296  ordtypelem4  9426  wdomima2g  9491  imadomg  10444  hashres  14361  hashimarn  14363  setsfun  17098  setsfun0  17099  lubfun  18273  glbfun  18286  qtoptop2  23643  volf  25486  nolesgn2ores  27640  nosupres  27675  nosupbnd2lem1  27683  noetasuplem4  27704  noetainflem4  27708  oniso  28267  bdayn0sf1o  28366  uhgrspansubgrlem  29363  upgrres  29379  umgrres  29380  hlimf  31312  fsuppcurry1  32803  fsuppcurry2  32804  eulerpartlemmf  34532  eulerpartlemgvv  34533  bj-funidres  37356  imadomfi  42256  funcoressn  47288  fundmdfat  47375  afvelrn  47414  dmfcoafv  47421  aovmpt4g  47447  fundmafv2rnb  47476