![]() |
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 6234 | . 2 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹) | |
2 | fndm 6235 | . . 3 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴) | |
3 | eqimss 3876 | . . 3 ⊢ (dom 𝐹 = 𝐴 → dom 𝐹 ⊆ 𝐴) | |
4 | 2, 3 | syl 17 | . 2 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 ⊆ 𝐴) |
5 | relssres 5687 | . 2 ⊢ ((Rel 𝐹 ∧ dom 𝐹 ⊆ 𝐴) → (𝐹 ↾ 𝐴) = 𝐹) | |
6 | 1, 4, 5 | syl2anc 579 | 1 ⊢ (𝐹 Fn 𝐴 → (𝐹 ↾ 𝐴) = 𝐹) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1601 ⊆ wss 3792 dom cdm 5355 ↾ cres 5357 Rel wrel 5360 Fn wfn 6130 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-13 2334 ax-ext 2754 ax-sep 5017 ax-nul 5025 ax-pr 5138 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-3an 1073 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-ral 3095 df-rex 3096 df-rab 3099 df-v 3400 df-dif 3795 df-un 3797 df-in 3799 df-ss 3806 df-nul 4142 df-if 4308 df-sn 4399 df-pr 4401 df-op 4405 df-br 4887 df-opab 4949 df-xp 5361 df-rel 5362 df-dm 5365 df-res 5367 df-fun 6137 df-fn 6138 |
This theorem is referenced by: fnima 6256 fresin 6323 resasplit 6324 fresaunres2 6326 fvreseq1 6581 fnsnr 6698 fninfp 6707 fnsnsplit 6721 fsnunfv 6724 fsnunres 6725 fnsuppeq0 7605 mapunen 8417 fnfi 8526 canthp1lem2 9810 fseq1p1m1 12732 facnn 13380 fac0 13381 hashgval 13438 hashinf 13440 rlimres 14697 lo1res 14698 rlimresb 14704 isercolllem2 14804 isercoll 14806 ruclem4 15367 fsets 16288 sscres 16868 sscid 16869 gsumzres 18696 pwssplit1 19454 zzngim 20296 ptuncnv 22019 ptcmpfi 22025 tsmsres 22355 imasdsf1olem 22586 tmslem 22695 tmsxms 22699 imasf1oxms 22702 prdsxms 22743 tmsxps 22749 tmsxpsmopn 22750 isngp2 22809 tngngp2 22864 cnfldms 22987 cncms 23561 cnfldcusp 23563 mbfres2 23849 dvres 24112 dvres3a 24115 cpnres 24137 dvmptres3 24156 dvlip2 24195 dvgt0lem2 24203 dvne0 24211 rlimcnp2 25145 jensen 25167 eupthvdres 27639 sspg 28155 ssps 28157 sspn 28163 hhsssh 28698 fnresin 29995 padct 30063 ffsrn 30070 resf1o 30071 gsumle 30341 cnrrext 30652 indf1ofs 30686 eulerpartlemt 31031 subfacp1lem3 31763 subfacp1lem5 31765 cvmliftlem11 31876 poimirlem9 34046 mapfzcons1 38244 eq0rabdioph 38304 eldioph4b 38339 diophren 38341 pwssplit4 38622 dvresntr 41064 sge0split 41554 |
Copyright terms: Public domain | W3C validator |