Theorem funres 6540

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

Syntax hints:   → wi 4   ⊆ wss 3889   ↾ cres 5633  Fun wfun 6492

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-in 3896  df-ss 3906  df-br 5086  df-opab 5148  df-rel 5638  df-cnv 5639  df-co 5640  df-res 5643  df-fun 6500

This theorem is referenced by:  funresd  6541  fores  6762  resfunexg  7170  funfvima  7185  funiunfv  7203  fprlem1  8250  smores  8292  smores2  8294  frfnom  8374  sbthlem7  9031  fsuppres  9306  ordtypelem4  9436  wdomima2g  9501  imadomg  10456  hashres  14400  hashimarn  14402  setsfun  17141  setsfun0  17142  lubfun  18316  glbfun  18329  qtoptop2  23664  volf  25496  nolesgn2ores  27636  nosupres  27671  nosupbnd2lem1  27679  noetasuplem4  27700  noetainflem4  27704  oniso  28263  bdayn0sf1o  28362  uhgrspansubgrlem  29359  upgrres  29375  umgrres  29376  hlimf  31308  fsuppcurry1  32797  fsuppcurry2  32798  eulerpartlemmf  34519  eulerpartlemgvv  34520  bj-funidres  37465  imadomfi  42441  funcoressn  47490  fundmdfat  47577  afvelrn  47616  dmfcoafv  47623  aovmpt4g  47649  fundmafv2rnb  47678