Theorem funres 6578

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

Syntax hints:   → wi 4   ⊆ wss 3905   ↾ cres 5663  Fun wfun 6530

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-in 3912  df-ss 3922  df-br 5110  df-opab 5174  df-rel 5668  df-cnv 5669  df-co 5670  df-res 5673  df-fun 6538

This theorem is referenced by:  funresd  6579  fores  6802  resfunexg  7213  funfvima  7228  funiunfv  7246  fprlem1  8293  smores  8335  smores2  8337  frfnom  8418  sbthlem7  9077  fsuppres  9349  ordtypelem4  9479  wdomima2g  9544  imadomg  10513  hashres  14471  hashimarn  14473  setsfun  17226  setsfun0  17227  lubfun  18401  glbfun  18414  qtoptop2  23856  volf  25688  nolesgn2ores  27836  nosupres  27871  nosupbnd2lem1  27879  noetasuplem4  27900  noetainflem4  27904  oniso  28464  bdayn0sf1o  28563  uhgrspansubgrlem  29640  upgrres  29656  umgrres  29657  hlimf  31589  fsuppcurry1  33069  fsuppcurry2  33070  eulerpartlemmf  34765  eulerpartlemgvv  34766  bj-funidres  37795  imadomfi  42769  funcoressn  47779  fundmdfat  47866  afvelrn  47905  dmfcoafv  47912  aovmpt4g  47938  fundmafv2rnb  47967