![]() |
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 6009 | . 2 ⊢ (𝐹 ↾ 𝐴) ⊆ 𝐹 | |
2 | funss 6575 | . 2 ⊢ ((𝐹 ↾ 𝐴) ⊆ 𝐹 → (Fun 𝐹 → Fun (𝐹 ↾ 𝐴))) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (Fun 𝐹 → Fun (𝐹 ↾ 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ⊆ wss 3947 ↾ cres 5682 Fun wfun 6545 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2698 |
This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1536 df-ex 1774 df-sb 2060 df-clab 2705 df-cleq 2719 df-clel 2805 df-v 3473 df-in 3954 df-ss 3964 df-br 5151 df-opab 5213 df-rel 5687 df-cnv 5688 df-co 5689 df-res 5692 df-fun 6553 |
This theorem is referenced by: funresd 6599 fores 6824 resfunexg 7231 funfvima 7246 funiunfv 7262 fprlem1 8310 wfrlem5OLD 8338 smores 8377 smores2 8379 frfnom 8460 sbthlem7 9118 fsuppres 9422 ordtypelem4 9550 wdomima2g 9615 imadomg 10563 hashres 14435 hashimarn 14437 setsfun 17145 setsfun0 17146 lubfun 18349 glbfun 18362 qtoptop2 23621 volf 25476 nolesgn2ores 27623 nosupres 27658 nosupbnd2lem1 27666 noetasuplem4 27687 noetainflem4 27691 uhgrspansubgrlem 29121 upgrres 29137 umgrres 29138 hlimf 31065 fsuppcurry1 32525 fsuppcurry2 32526 eulerpartlemmf 34000 eulerpartlemgvv 34001 bj-funidres 36635 imadomfi 41477 funcoressn 46426 fundmdfat 46511 afvelrn 46550 dmfcoafv 46557 aovmpt4g 46583 fundmafv2rnb 46612 |
Copyright terms: Public domain | W3C validator |