MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  funresd Structured version   Visualization version   GIF version

Theorem funresd 6592
Description: A restriction of a function is a function. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
Hypothesis
Ref Expression
funresd.1 (𝜑 → Fun 𝐹)
Assertion
Ref Expression
funresd (𝜑 → Fun (𝐹𝐴))

Proof of Theorem funresd
StepHypRef Expression
1 funresd.1 . 2 (𝜑 → Fun 𝐹)
2 funres 6591 . 2 (Fun 𝐹 → Fun (𝐹𝐴))
31, 2syl 17 1 (𝜑 → Fun (𝐹𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  cres 5679  Fun wfun 6538
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966  df-br 5150  df-opab 5212  df-rel 5684  df-cnv 5685  df-co 5686  df-res 5689  df-fun 6546
This theorem is referenced by:  fnssresb  6673  respreima  7068  frrlem11  8281  frrlem12  8282  frrlem15  9752  gsumzadd  19790  gsum2dlem2  19839  nogesgn1ores  27177  noinfres  27225  noinfbnd2lem1  27233  trlsegvdeglem2  29474  sspg  29981  ssps  29983  sspn  29989  fresf1o  31855  fsupprnfi  31914  gsumhashmul  32208  limsupresxr  44482  liminfresxr  44483  afvco2  45884
  Copyright terms: Public domain W3C validator