![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > fnresdm | Structured version Visualization version Unicode version |
Description: A function does not change when restricted to its domain. (Contributed by NM, 5-Sep-2004.) |
Ref | Expression |
---|---|
fnresdm |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fnrel 5695 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | fndm 5696 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | eqimss 3495 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | syl 17 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | relssres 5160 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | 1, 4, 5 | syl2anc 671 |
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-dm 4862 df-res 4864 df-fun 5602 df-fn 5603 |
This theorem is referenced by: fnima 5715 fresin 5774 resasplit 5775 fresaunres2 5777 fvreseq1 6005 fnsnb 6106 fninfp 6114 fnsnsplit 6124 fsnunfv 6127 fsnunres 6128 fnsuppeq0 6969 mapunen 7766 fnfi 7874 canthp1lem2 9103 fseq1p1m1 11896 facnn 12492 fac0 12493 hashgval 12549 hashinf 12551 rlimres 13670 lo1res 13671 rlimresb 13677 isercolllem2 13777 isercoll 13779 ruclem4 14334 fsets 15197 sscres 15776 sscid 15777 gsumzres 17591 pwssplit1 18330 zzngim 19171 ptuncnv 20870 ptcmpfi 20876 tsmsres 21206 imasdsf1olem 21436 tmslem 21545 tmsxms 21549 imasf1oxms 21552 prdsxms 21593 tmsxps 21599 tmsxpsmopn 21600 isngp2 21659 tngngp2 21708 cnfldms 21844 cncms 22370 cnfldcusp 22372 mbfres2 22649 dvres 22914 dvres3a 22917 cpnres 22939 dvmptres3 22958 dvlip2 22995 dvgt0lem2 23003 dvne0 23011 rlimcnp2 23940 jensen 23962 eupath2 25756 subgores 26080 sspg 26415 ssps 26417 sspn 26423 hhsssh 26968 fnresin 28276 padct 28355 ffsrn 28362 resf1o 28363 gsumle 28590 cnrrext 28862 indf1ofs 28895 eulerpartlemt 29252 bnj142OLD 29582 subfacp1lem3 29953 subfacp1lem5 29955 cvmliftlem11 30066 poimirlem9 31993 mapfzcons1 35603 eq0rabdioph 35663 eldioph4b 35698 diophren 35700 pwssplit4 35991 dvresntr 37825 sge0split 38288 |
Copyright terms: Public domain | W3C validator |