Theorem funres 6524

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

Syntax hints:   → wi 4   ⊆ wss 3903   ↾ cres 5621  Fun wfun 6476

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 3438  df-in 3910  df-ss 3920  df-br 5093  df-opab 5155  df-rel 5626  df-cnv 5627  df-co 5628  df-res 5631  df-fun 6484

This theorem is referenced by:  funresd  6525  fores  6746  resfunexg  7151  funfvima  7166  funiunfv  7184  fprlem1  8233  smores  8275  smores2  8277  frfnom  8357  sbthlem7  9010  fsuppres  9283  ordtypelem4  9413  wdomima2g  9478  imadomg  10428  hashres  14345  hashimarn  14347  setsfun  17082  setsfun0  17083  lubfun  18256  glbfun  18269  qtoptop2  23584  volf  25428  nolesgn2ores  27582  nosupres  27617  nosupbnd2lem1  27625  noetasuplem4  27646  noetainflem4  27650  onsiso  28174  bdayn0sf1o  28264  uhgrspansubgrlem  29235  upgrres  29251  umgrres  29252  hlimf  31181  fsuppcurry1  32669  fsuppcurry2  32670  eulerpartlemmf  34349  eulerpartlemgvv  34350  bj-funidres  37135  imadomfi  41985  funcoressn  47036  fundmdfat  47123  afvelrn  47162  dmfcoafv  47169  aovmpt4g  47195  fundmafv2rnb  47224