Theorem funres 6528

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

Syntax hints:   → wi 4   ⊆ wss 3905   ↾ cres 5625  Fun wfun 6480

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 3440  df-in 3912  df-ss 3922  df-br 5096  df-opab 5158  df-rel 5630  df-cnv 5631  df-co 5632  df-res 5635  df-fun 6488

This theorem is referenced by:  funresd  6529  fores  6750  resfunexg  7155  funfvima  7170  funiunfv  7188  fprlem1  8240  smores  8282  smores2  8284  frfnom  8364  sbthlem7  9017  fsuppres  9302  ordtypelem4  9432  wdomima2g  9497  imadomg  10447  hashres  14363  hashimarn  14365  setsfun  17100  setsfun0  17101  lubfun  18274  glbfun  18287  qtoptop2  23602  volf  25446  nolesgn2ores  27600  nosupres  27635  nosupbnd2lem1  27643  noetasuplem4  27664  noetainflem4  27668  onsiso  28192  bdayn0sf1o  28282  uhgrspansubgrlem  29253  upgrres  29269  umgrres  29270  hlimf  31199  fsuppcurry1  32681  fsuppcurry2  32682  eulerpartlemmf  34345  eulerpartlemgvv  34346  bj-funidres  37127  imadomfi  41978  funcoressn  47030  fundmdfat  47117  afvelrn  47156  dmfcoafv  47163  aovmpt4g  47189  fundmafv2rnb  47218