Theorem funres 6561

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

Syntax hints:   → wi 4   ⊆ wss 3917   ↾ cres 5643  Fun wfun 6508

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-in 3924  df-ss 3934  df-br 5111  df-opab 5173  df-rel 5648  df-cnv 5649  df-co 5650  df-res 5653  df-fun 6516

This theorem is referenced by:  funresd  6562  fores  6785  resfunexg  7192  funfvima  7207  funiunfv  7225  fprlem1  8282  smores  8324  smores2  8326  frfnom  8406  sbthlem7  9063  fsuppres  9351  ordtypelem4  9481  wdomima2g  9546  imadomg  10494  hashres  14410  hashimarn  14412  setsfun  17148  setsfun0  17149  lubfun  18318  glbfun  18331  qtoptop2  23593  volf  25437  nolesgn2ores  27591  nosupres  27626  nosupbnd2lem1  27634  noetasuplem4  27655  noetainflem4  27659  onsiso  28176  bdayn0sf1o  28266  uhgrspansubgrlem  29224  upgrres  29240  umgrres  29241  hlimf  31173  fsuppcurry1  32655  fsuppcurry2  32656  eulerpartlemmf  34373  eulerpartlemgvv  34374  bj-funidres  37146  imadomfi  41997  funcoressn  47047  fundmdfat  47134  afvelrn  47173  dmfcoafv  47180  aovmpt4g  47206  fundmafv2rnb  47235