Theorem funres 6542

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

Syntax hints:   → wi 4   ⊆ wss 3903   ↾ cres 5634  Fun wfun 6494

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 3444  df-in 3910  df-ss 3920  df-br 5101  df-opab 5163  df-rel 5639  df-cnv 5640  df-co 5641  df-res 5644  df-fun 6502

This theorem is referenced by:  funresd  6543  fores  6764  resfunexg  7171  funfvima  7186  funiunfv  7204  fprlem1  8252  smores  8294  smores2  8296  frfnom  8376  sbthlem7  9033  fsuppres  9308  ordtypelem4  9438  wdomima2g  9503  imadomg  10456  hashres  14373  hashimarn  14375  setsfun  17110  setsfun0  17111  lubfun  18285  glbfun  18298  qtoptop2  23655  volf  25498  nolesgn2ores  27652  nosupres  27687  nosupbnd2lem1  27695  noetasuplem4  27716  noetainflem4  27720  oniso  28279  bdayn0sf1o  28378  uhgrspansubgrlem  29375  upgrres  29391  umgrres  29392  hlimf  31324  fsuppcurry1  32813  fsuppcurry2  32814  eulerpartlemmf  34552  eulerpartlemgvv  34553  bj-funidres  37403  imadomfi  42369  funcoressn  47399  fundmdfat  47486  afvelrn  47525  dmfcoafv  47532  aovmpt4g  47558  fundmafv2rnb  47587