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

Theorem funres 6146
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
StepHypRef Expression
1 resss 5632 . 2 (𝐹𝐴) ⊆ 𝐹
2 funss 6123 . 2 ((𝐹𝐴) ⊆ 𝐹 → (Fun 𝐹 → Fun (𝐹𝐴)))
31, 2ax-mp 5 1 (Fun 𝐹 → Fun (𝐹𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wss 3776  cres 5320  Fun wfun 6098
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2791
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2800  df-cleq 2806  df-clel 2809  df-nfc 2944  df-v 3400  df-in 3783  df-ss 3790  df-br 4852  df-opab 4914  df-rel 5325  df-cnv 5326  df-co 5327  df-res 5330  df-fun 6106
This theorem is referenced by:  fnssresb  6217  fnresi  6222  fores  6343  respreima  6569  resfunexg  6707  funfvima  6720  funiunfv  6733  wfrlem5  7658  smores  7688  smores2  7690  frfnom  7769  sbthlem7  8318  fsuppres  8542  ordtypelem4  8668  wdomima2g  8733  imadomg  9644  hashres  13445  hashimarn  13447  setsfun  16107  setsfun0  16108  lubfun  17188  glbfun  17201  gsumzadd  18526  gsum2dlem2  18574  qtoptop2  21720  volf  23516  uhgrspansubgrlem  26404  upgrres  26420  umgrres  26421  trlsegvdeglem2  27400  sspg  27917  ssps  27919  sspn  27925  hlimf  28428  fresf1o  29766  eulerpartlemmf  30768  eulerpartlemgvv  30769  frrlem5  32110  nolesgn2ores  32151  nosupres  32179  nosupbnd2lem1  32187  noetalem3  32191  funresd  39960  funcoressn  41662  fundmdfat  41719  afvelrn  41758  dmfcoafv  41765  afvco2  41766  aovmpt4g  41791  fundmafv2rnb  41820
  Copyright terms: Public domain W3C validator