| 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 6019 | . 2 ⊢ (𝐹 ↾ 𝐴) ⊆ 𝐹 | |
| 2 | funss 6585 | . 2 ⊢ ((𝐹 ↾ 𝐴) ⊆ 𝐹 → (Fun 𝐹 → Fun (𝐹 ↾ 𝐴))) | |
| 3 | 1, 2 | ax-mp 5 | 1 ⊢ (Fun 𝐹 → Fun (𝐹 ↾ 𝐴)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ⊆ wss 3951 ↾ cres 5687 Fun wfun 6555 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3482 df-in 3958 df-ss 3968 df-br 5144 df-opab 5206 df-rel 5692 df-cnv 5693 df-co 5694 df-res 5697 df-fun 6563 |
| This theorem is referenced by: funresd 6609 fores 6830 resfunexg 7235 funfvima 7250 funiunfv 7268 fprlem1 8325 wfrlem5OLD 8353 smores 8392 smores2 8394 frfnom 8475 sbthlem7 9129 fsuppres 9433 ordtypelem4 9561 wdomima2g 9626 imadomg 10574 hashres 14477 hashimarn 14479 setsfun 17208 setsfun0 17209 lubfun 18397 glbfun 18410 qtoptop2 23707 volf 25564 nolesgn2ores 27717 nosupres 27752 nosupbnd2lem1 27760 noetasuplem4 27781 noetainflem4 27785 uhgrspansubgrlem 29307 upgrres 29323 umgrres 29324 hlimf 31256 fsuppcurry1 32736 fsuppcurry2 32737 eulerpartlemmf 34377 eulerpartlemgvv 34378 bj-funidres 37152 imadomfi 42003 funcoressn 47054 fundmdfat 47141 afvelrn 47180 dmfcoafv 47187 aovmpt4g 47213 fundmafv2rnb 47242 |
| Copyright terms: Public domain | W3C validator |