![]() |
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 5717 | . 2 ⊢ (𝐹 ↾ 𝐴) ⊆ 𝐹 | |
2 | funss 6201 | . 2 ⊢ ((𝐹 ↾ 𝐴) ⊆ 𝐹 → (Fun 𝐹 → Fun (𝐹 ↾ 𝐴))) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (Fun 𝐹 → Fun (𝐹 ↾ 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ⊆ wss 3825 ↾ cres 5402 Fun wfun 6176 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1964 ax-8 2050 ax-9 2057 ax-10 2077 ax-11 2091 ax-12 2104 ax-ext 2745 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2014 df-clab 2754 df-cleq 2765 df-clel 2840 df-nfc 2912 df-v 3411 df-in 3832 df-ss 3839 df-br 4924 df-opab 4986 df-rel 5407 df-cnv 5408 df-co 5409 df-res 5412 df-fun 6184 |
This theorem is referenced by: fnssresb 6296 fnresi 6301 fores 6423 respreima 6655 resfunexg 6798 funfvima 6812 funiunfv 6826 wfrlem5 7756 smores 7786 smores2 7788 frfnom 7867 sbthlem7 8421 fsuppres 8645 ordtypelem4 8772 wdomima2g 8837 imadomg 9746 hashres 13602 hashimarn 13604 setsfun 16364 setsfun0 16365 lubfun 17438 glbfun 17451 gsumzadd 18785 gsum2dlem2 18834 qtoptop2 22001 volf 23823 uhgrspansubgrlem 26765 upgrres 26781 umgrres 26782 trlsegvdeglem2 27741 sspg 28272 ssps 28274 sspn 28280 hlimf 28783 fresf1o 30129 fsuppcurry1 30202 fsuppcurry2 30203 eulerpartlemmf 31235 eulerpartlemgvv 31236 frrlem11 32594 frrlem12 32595 fprlem1 32598 frrlem15 32603 nolesgn2ores 32640 nosupres 32668 nosupbnd2lem1 32676 noetalem3 32680 funresd 40907 funcoressn 42628 fundmdfat 42680 afvelrn 42719 dmfcoafv 42726 afvco2 42727 aovmpt4g 42752 fundmafv2rnb 42781 |
Copyright terms: Public domain | W3C validator |