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

Theorem funresd 6545
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 6544 . 2 (Fun 𝐹 → Fun (𝐹𝐴))
31, 2syl 17 1 (𝜑 → Fun (𝐹𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  cres 5636  Fun wfun 6491
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 3446  df-in 3918  df-ss 3928  df-br 5107  df-opab 5169  df-rel 5641  df-cnv 5642  df-co 5643  df-res 5646  df-fun 6499
This theorem is referenced by:  fnssresb  6624  respreima  7017  frrlem11  8228  frrlem12  8229  frrlem15  9698  gsumzadd  19704  gsum2dlem2  19753  nogesgn1ores  27038  noinfres  27086  noinfbnd2lem1  27094  trlsegvdeglem2  29207  sspg  29712  ssps  29714  sspn  29720  fresf1o  31591  fsupprnfi  31653  gsumhashmul  31947  limsupresxr  44093  liminfresxr  44094  afvco2  45494
  Copyright terms: Public domain W3C validator