Theorem funres 6598

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

Syntax hints:   → wi 4   ⊆ wss 3947   ↾ cres 5682  Fun wfun 6545

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2698

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2705  df-cleq 2719  df-clel 2805  df-v 3473  df-in 3954  df-ss 3964  df-br 5151  df-opab 5213  df-rel 5687  df-cnv 5688  df-co 5689  df-res 5692  df-fun 6553

This theorem is referenced by:  funresd  6599  fores  6824  resfunexg  7231  funfvima  7246  funiunfv  7262  fprlem1  8310  wfrlem5OLD  8338  smores  8377  smores2  8379  frfnom  8460  sbthlem7  9118  fsuppres  9422  ordtypelem4  9550  wdomima2g  9615  imadomg  10563  hashres  14435  hashimarn  14437  setsfun  17145  setsfun0  17146  lubfun  18349  glbfun  18362  qtoptop2  23621  volf  25476  nolesgn2ores  27623  nosupres  27658  nosupbnd2lem1  27666  noetasuplem4  27687  noetainflem4  27691  uhgrspansubgrlem  29121  upgrres  29137  umgrres  29138  hlimf  31065  fsuppcurry1  32525  fsuppcurry2  32526  eulerpartlemmf  34000  eulerpartlemgvv  34001  bj-funidres  36635  imadomfi  41477  funcoressn  46426  fundmdfat  46511  afvelrn  46550  dmfcoafv  46557  aovmpt4g  46583  fundmafv2rnb  46612