Theorem funres 6583

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3895   ↾ cres 5652  Fun wfun 6533

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3896  df-in 4091  df-br 5103  df-opab 5167  df-rel 5657  df-cnv 5658  df-co 5659  df-res 5662  df-fun 6541

This theorem is used by:  funresd  6584  fores  6807  resfunexg  7222  funfvima  7237  funiunfv  7253  fprlem1  8322  smores  8364  smores2  8366  frfnom  8447  sbthlem7  9116  fsuppres  9389  ordtypelem4  9519  wdomima2g  9584  imadomg  10617  imadomnum  10618  hashres  14587  hashimarn  14589  setsfun  17355  setsfun0  17356  lubfun  18530  glbfun  18543  qtoptop2  24024  volf  25856  nolesgn2ores  28035  nosupres  28070  nosupbnd2lem1  28078  noetasuplem4  28099  noetainflem4  28103  oniso  28663  bdayn0sf1o  28762  uhgrspansubgrlem  29877  upgrres  29893  umgrres  29894  hlimf  31845  fsuppcurry1  33363  fsuppcurry2  33364  eulerpartlemmf  35054  eulerpartlemgvv  35055  srepdflem1  36005  bj-funidres  38166  imadomfi  43146  funcoressn  48206  fundmdfat  48293  afvelrn  48332  dmfcoafv  48339  aovmpt4g  48365  fundmafv2rnb  48394