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

Theorem funres 5826
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 5326 . 2 (𝐹𝐴) ⊆ 𝐹
2 funss 5805 . 2 ((𝐹𝐴) ⊆ 𝐹 → (Fun 𝐹 → Fun (𝐹𝐴)))
31, 2ax-mp 5 1 (Fun 𝐹 → Fun (𝐹𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wss 3536  cres 5027  Fun wfun 5781
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-v 3171  df-in 3543  df-ss 3550  df-br 4575  df-opab 4635  df-rel 5032  df-cnv 5033  df-co 5034  df-res 5037  df-fun 5789
This theorem is referenced by:  fnssresb  5900  fnresi  5905  fores  6019  respreima  6234  resfunexg  6359  funfvima  6371  funiunfv  6385  wfrlem5  7280  smores  7310  smores2  7312  frfnom  7391  sbthlem7  7935  fsuppres  8157  ordtypelem4  8283  wdomima2g  8348  imadomg  9211  hashimarn  13034  setsfun  15668  setsfun0  15669  lubfun  16746  glbfun  16759  gsumzadd  18088  gsum2dlem2  18136  qtoptop2  21251  volf  23018  sspg  26768  ssps  26770  sspn  26776  hlimf  27281  fresf1o  28618  eulerpartlemmf  29567  eulerpartlemgvv  29568  frrlem5  30831  funcoressn  39657  afvelrn  39699  dmfcoafv  39706  afvco2  39707  aovmpt4g  39732  uhgrspansubgrlem  40513  trlsegvdeglem2  41388
  Copyright terms: Public domain W3C validator