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 3890   ↾ 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 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-in 3897  df-ss 3907  df-br 5087  df-opab 5149  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  7163  funfvima  7178  funiunfv  7196  fprlem1  8243  smores  8285  smores2  8287  frfnom  8367  sbthlem7  9024  fsuppres  9299  ordtypelem4  9429  wdomima2g  9494  imadomg  10447  hashres  14391  hashimarn  14393  setsfun  17132  setsfun0  17133  lubfun  18307  glbfun  18320  qtoptop2  23674  volf  25506  nolesgn2ores  27650  nosupres  27685  nosupbnd2lem1  27693  noetasuplem4  27714  noetainflem4  27718  oniso  28277  bdayn0sf1o  28376  uhgrspansubgrlem  29373  upgrres  29389  umgrres  29390  hlimf  31323  fsuppcurry1  32812  fsuppcurry2  32813  eulerpartlemmf  34535  eulerpartlemgvv  34536  bj-funidres  37481  imadomfi  42455  funcoressn  47502  fundmdfat  47589  afvelrn  47628  dmfcoafv  47635  aovmpt4g  47661  fundmafv2rnb  47690