Theorem funres 6558

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

Syntax hints:   → wi 4   ⊆ wss 3914   ↾ cres 5640  Fun wfun 6505

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-in 3921  df-ss 3931  df-br 5108  df-opab 5170  df-rel 5645  df-cnv 5646  df-co 5647  df-res 5650  df-fun 6513

This theorem is referenced by:  funresd  6559  fores  6782  resfunexg  7189  funfvima  7204  funiunfv  7222  fprlem1  8279  smores  8321  smores2  8323  frfnom  8403  sbthlem7  9057  fsuppres  9344  ordtypelem4  9474  wdomima2g  9539  imadomg  10487  hashres  14403  hashimarn  14405  setsfun  17141  setsfun0  17142  lubfun  18311  glbfun  18324  qtoptop2  23586  volf  25430  nolesgn2ores  27584  nosupres  27619  nosupbnd2lem1  27627  noetasuplem4  27648  noetainflem4  27652  onsiso  28169  bdayn0sf1o  28259  uhgrspansubgrlem  29217  upgrres  29233  umgrres  29234  hlimf  31166  fsuppcurry1  32648  fsuppcurry2  32649  eulerpartlemmf  34366  eulerpartlemgvv  34367  bj-funidres  37139  imadomfi  41990  funcoressn  47043  fundmdfat  47130  afvelrn  47169  dmfcoafv  47176  aovmpt4g  47202  fundmafv2rnb  47231