Theorem funres 6527

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

Syntax hints:   → wi 4   ⊆ wss 3883   ↾ cres 5620  Fun wfun 6479

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-in 3890  df-ss 3900  df-br 5073  df-opab 5135  df-rel 5625  df-cnv 5626  df-co 5627  df-res 5630  df-fun 6487

This theorem is referenced by:  funresd  6528  fores  6749  resfunexg  7159  funfvima  7174  funiunfv  7192  fprlem1  8240  smores  8282  smores2  8284  frfnom  8364  sbthlem7  9021  fsuppres  9296  ordtypelem4  9426  wdomima2g  9491  imadomg  10447  hashres  14391  hashimarn  14393  setsfun  17132  setsfun0  17133  lubfun  18307  glbfun  18320  qtoptop2  23682  volf  25514  nolesgn2ores  27654  nosupres  27689  nosupbnd2lem1  27697  noetasuplem4  27718  noetainflem4  27722  oniso  28281  bdayn0sf1o  28380  uhgrspansubgrlem  29377  upgrres  29393  umgrres  29394  hlimf  31326  fsuppcurry1  32816  fsuppcurry2  32817  eulerpartlemmf  34559  eulerpartlemgvv  34560  bj-funidres  37511  imadomfi  42487  funcoressn  47505  fundmdfat  47592  afvelrn  47631  dmfcoafv  47638  aovmpt4g  47664  fundmafv2rnb  47693