Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > fnresdm | Structured version Visualization version GIF version |
Description: A function does not change when restricted to its domain. (Contributed by NM, 5-Sep-2004.) |
Ref | Expression |
---|---|
fnresdm | ⊢ (𝐹 Fn 𝐴 → (𝐹 ↾ 𝐴) = 𝐹) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fnrel 6447 | . 2 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹) | |
2 | fndm 6448 | . . 3 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴) | |
3 | eqimss 4020 | . . 3 ⊢ (dom 𝐹 = 𝐴 → dom 𝐹 ⊆ 𝐴) | |
4 | 2, 3 | syl 17 | . 2 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 ⊆ 𝐴) |
5 | relssres 5886 | . 2 ⊢ ((Rel 𝐹 ∧ dom 𝐹 ⊆ 𝐴) → (𝐹 ↾ 𝐴) = 𝐹) | |
6 | 1, 4, 5 | syl2anc 584 | 1 ⊢ (𝐹 Fn 𝐴 → (𝐹 ↾ 𝐴) = 𝐹) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1528 ⊆ wss 3933 dom cdm 5548 ↾ cres 5550 Rel wrel 5553 Fn wfn 6343 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 ax-sep 5194 ax-nul 5201 ax-pr 5320 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-ral 3140 df-rex 3141 df-rab 3144 df-v 3494 df-dif 3936 df-un 3938 df-in 3940 df-ss 3949 df-nul 4289 df-if 4464 df-sn 4558 df-pr 4560 df-op 4564 df-br 5058 df-opab 5120 df-xp 5554 df-rel 5555 df-dm 5558 df-res 5560 df-fun 6350 df-fn 6351 |
This theorem is referenced by: fnima 6471 fresin 6540 resasplit 6541 fresaunres2 6543 fvreseq1 6801 fnsnr 6919 fninfp 6928 fnsnsplit 6938 fsnunfv 6941 fsnunres 6942 fnsuppeq0 7847 mapunen 8674 fnfi 8784 canthp1lem2 10063 fseq1p1m1 12969 facnn 13623 fac0 13624 hashgval 13681 hashinf 13683 rlimres 14903 lo1res 14904 rlimresb 14910 isercolllem2 15010 isercoll 15012 ruclem4 15575 fsets 16504 sscres 17081 sscid 17082 gsumzres 18958 rnrhmsubrg 19496 pwssplit1 19760 zzngim 20627 ptuncnv 22343 ptcmpfi 22349 tsmsres 22679 imasdsf1olem 22910 tmslem 23019 tmsxms 23023 imasf1oxms 23026 prdsxms 23067 tmsxps 23073 tmsxpsmopn 23074 isngp2 23133 tngngp2 23188 cnfldms 23311 cncms 23885 cnfldcusp 23887 mbfres2 24173 dvres 24436 dvres3a 24439 cpnres 24461 dvmptres3 24480 dvlip2 24519 dvgt0lem2 24527 dvne0 24535 rlimcnp2 25471 jensen 25493 eupthvdres 27941 sspg 28432 ssps 28434 sspn 28440 hhsssh 28973 fnresin 30299 padct 30381 ffsrn 30391 resf1o 30392 gsumle 30652 symgcom 30654 cycpmconjvlem 30710 cycpmconjslem1 30723 cnrrext 31150 indf1ofs 31184 eulerpartlemt 31528 subfacp1lem3 32326 subfacp1lem5 32328 cvmliftlem11 32439 poimirlem9 34782 mapfzcons1 39192 eq0rabdioph 39251 eldioph4b 39286 diophren 39288 pwssplit4 39567 dvresntr 42078 sge0split 42568 |
Copyright terms: Public domain | W3C validator |