![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > fssres | Structured version Visualization version Unicode version |
Description: Restriction of a function with a subclass of its domain. (Contributed by NM, 23-Sep-2004.) |
Ref | Expression |
---|---|
fssres |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-f 5604 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | fnssres 5710 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | resss 5146 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | rnss 5081 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 3, 4 | ax-mp 5 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | sstr 3451 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | 5, 6 | mpan 681 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | 2, 7 | anim12i 574 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
9 | 8 | an32s 818 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
10 | 1, 9 | sylanb 479 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
11 | df-f 5604 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
12 | 10, 11 | sylibr 217 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1679 ax-4 1692 ax-5 1768 ax-6 1815 ax-7 1861 ax-9 1906 ax-10 1925 ax-11 1930 ax-12 1943 ax-13 2101 ax-ext 2441 ax-sep 4538 ax-nul 4547 ax-pr 4652 |
This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3an 993 df-tru 1457 df-ex 1674 df-nf 1678 df-sb 1808 df-clab 2448 df-cleq 2454 df-clel 2457 df-nfc 2591 df-ne 2634 df-ral 2753 df-rex 2754 df-rab 2757 df-v 3058 df-dif 3418 df-un 3420 df-in 3422 df-ss 3429 df-nul 3743 df-if 3893 df-sn 3980 df-pr 3982 df-op 3986 df-br 4416 df-opab 4475 df-xp 4858 df-rel 4859 df-cnv 4860 df-co 4861 df-dm 4862 df-rn 4863 df-res 4864 df-fun 5602 df-fn 5603 df-f 5604 |
This theorem is referenced by: fssresd 5772 fssres2 5773 fresin 5774 fresaun 5776 f1ssres 5808 f2ndf 6928 elmapssres 7521 pmresg 7524 ralxpmap 7546 mapunen 7766 fofinf1o 7877 fseqenlem1 8480 inar1 9225 gruima 9252 addnqf 9398 mulnqf 9399 fseq1p1m1 11896 injresinj 12056 seqf1olem2 12284 rlimres 13670 lo1res 13671 vdwnnlem1 14993 fsets 15197 resmhm 16654 resghm 16947 gsumzres 17591 gsumzadd 17603 gsum2dlem2 17651 dpjidcl 17739 ablfac1eu 17754 abvres 18115 znf1o 19170 islindf4 19444 kgencn 20619 ptrescn 20702 hmeores 20834 tsmsres 21206 tsmsmhm 21208 tsmsadd 21209 xrge0gsumle 21899 xrge0tsms 21900 ovolicc2lem4OLD 22521 ovolicc2lem4 22522 limcdif 22879 limcflf 22884 limcmo 22885 dvres 22914 dvres3a 22917 aannenlem1 23332 logcn 23640 dvlog 23644 dvlog2 23646 logtayl 23653 dvatan 23909 atancn 23910 efrlim 23943 amgm 23964 dchrelbas2 24213 redwlk 25384 issubgoi 26086 hhssnv 26963 xrge0tsmsd 28596 cntmeas 29096 eulerpartlemt 29252 eulerpartlemmf 29256 eulerpartlemgvv 29257 subiwrd 29266 sseqp1 29276 wrdres 29474 poimirlem4 31988 mbfresfi 32031 mbfposadd 32032 itg2gt0cn 32041 sdclem2 32115 mzpcompact2lem 35637 eldiophb 35643 eldioph2 35648 cncfiooicclem1 37808 fouriersw 38132 sge0tsms 38259 psmeasure 38346 wrdred1 38957 red1wlklem 39715 pthdivtx 39761 resmgmhm 40070 lindslinindimp2lem2 40524 |
Copyright terms: Public domain | W3C validator |