Theorem funres 5929

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

Syntax hints:   → wi 4   ⊆ wss 3574   ↾ cres 5116  Fun wfun 5882

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-in 3581  df-ss 3588  df-br 4654  df-opab 4713  df-rel 5121  df-cnv 5122  df-co 5123  df-res 5126  df-fun 5890

This theorem is referenced by:  fnssresb  6003  fnresi  6008  fores  6124  respreima  6344  resfunexg  6479  funfvima  6492  funiunfv  6506  wfrlem5  7419  smores  7449  smores2  7451  frfnom  7530  sbthlem7  8076  fsuppres  8300  ordtypelem4  8426  wdomima2g  8491  imadomg  9356  hashres  13225  hashimarn  13227  setsfun  15893  setsfun0  15894  lubfun  16980  glbfun  16993  gsumzadd  18322  gsum2dlem2  18370  qtoptop2  21502  volf  23297  uhgrspansubgrlem  26182  upgrres  26198  umgrres  26199  trlsegvdeglem2  27081  sspg  27583  ssps  27585  sspn  27591  hlimf  28094  fresf1o  29433  eulerpartlemmf  30437  eulerpartlemgvv  30438  frrlem5  31784  nolesgn2ores  31825  nosupres  31853  nosupbnd2lem1  31861  noetalem3  31865  funresd  39476  funcoressn  41207  afvelrn  41248  dmfcoafv  41255  afvco2  41256  aovmpt4g  41281