Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > funres | Structured version Visualization version GIF version |
Description: A restriction of a function is a function. Compare Exercise 18 of [TakeutiZaring] p. 25. (Contributed by NM, 16-Aug-1994.) |
Ref | Expression |
---|---|
funres | ⊢ (Fun 𝐹 → Fun (𝐹 ↾ 𝐴)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | resss 5871 | . 2 ⊢ (𝐹 ↾ 𝐴) ⊆ 𝐹 | |
2 | funss 6367 | . 2 ⊢ ((𝐹 ↾ 𝐴) ⊆ 𝐹 → (Fun 𝐹 → Fun (𝐹 ↾ 𝐴))) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (Fun 𝐹 → Fun (𝐹 ↾ 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ⊆ wss 3933 ↾ cres 5550 Fun wfun 6342 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-v 3494 df-in 3940 df-ss 3949 df-br 5058 df-opab 5120 df-rel 5555 df-cnv 5556 df-co 5557 df-res 5560 df-fun 6350 |
This theorem is referenced by: fnssresb 6462 fnresiOLD 6470 fores 6593 respreima 6828 resfunexg 6969 funfvima 6983 funiunfv 6998 wfrlem5 7948 smores 7978 smores2 7980 frfnom 8059 sbthlem7 8621 fsuppres 8846 ordtypelem4 8973 wdomima2g 9038 imadomg 9944 hashres 13787 hashimarn 13789 setsfun 16506 setsfun0 16507 lubfun 17578 glbfun 17591 gsumzadd 18971 gsum2dlem2 19020 qtoptop2 22235 volf 24057 uhgrspansubgrlem 26999 upgrres 27015 umgrres 27016 trlsegvdeglem2 27927 sspg 28432 ssps 28434 sspn 28440 hlimf 28941 fresf1o 30304 fsuppcurry1 30387 fsuppcurry2 30388 eulerpartlemmf 31532 eulerpartlemgvv 31533 frrlem11 33030 frrlem12 33031 fprlem1 33034 frrlem15 33039 nolesgn2ores 33076 nosupres 33104 nosupbnd2lem1 33112 noetalem3 33116 bj-funidres 34335 funresd 41409 funcoressn 43154 fundmdfat 43205 afvelrn 43244 dmfcoafv 43251 afvco2 43252 aovmpt4g 43277 fundmafv2rnb 43306 |
Copyright terms: Public domain | W3C validator |