![]() |
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 6424 | . 2 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹) | |
2 | fndm 6425 | . . 3 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴) | |
3 | eqimss 3971 | . . 3 ⊢ (dom 𝐹 = 𝐴 → dom 𝐹 ⊆ 𝐴) | |
4 | 2, 3 | syl 17 | . 2 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 ⊆ 𝐴) |
5 | relssres 5859 | . 2 ⊢ ((Rel 𝐹 ∧ dom 𝐹 ⊆ 𝐴) → (𝐹 ↾ 𝐴) = 𝐹) | |
6 | 1, 4, 5 | syl2anc 587 | 1 ⊢ (𝐹 Fn 𝐴 → (𝐹 ↾ 𝐴) = 𝐹) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1538 ⊆ wss 3881 dom cdm 5519 ↾ cres 5521 Rel wrel 5524 Fn wfn 6319 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 ax-sep 5167 ax-nul 5174 ax-pr 5295 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3an 1086 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-ral 3111 df-rex 3112 df-v 3443 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-nul 4244 df-if 4426 df-sn 4526 df-pr 4528 df-op 4532 df-br 5031 df-opab 5093 df-xp 5525 df-rel 5526 df-dm 5529 df-res 5531 df-fun 6326 df-fn 6327 |
This theorem is referenced by: fnima 6450 fresin 6521 resasplit 6522 fresaunres2 6524 fvreseq1 6786 fnsnr 6904 fninfp 6913 fnsnsplit 6923 fsnunfv 6926 fsnunres 6927 fnsuppeq0 7841 mapunen 8670 fnfi 8780 canthp1lem2 10064 fseq1p1m1 12976 facnn 13631 fac0 13632 hashgval 13689 hashinf 13691 rlimres 14907 lo1res 14908 rlimresb 14914 isercolllem2 15014 isercoll 15016 ruclem4 15579 fsets 16508 sscres 17085 sscid 17086 gsumzres 19022 rnrhmsubrg 19560 pwssplit1 19824 zzngim 20244 ptuncnv 22412 ptcmpfi 22418 tsmsres 22749 imasdsf1olem 22980 tmslem 23089 tmsxms 23093 imasf1oxms 23096 prdsxms 23137 tmsxps 23143 tmsxpsmopn 23144 isngp2 23203 tngngp2 23258 cnfldms 23381 cncms 23959 cnfldcusp 23961 mbfres2 24249 dvres 24514 dvres3a 24517 cpnres 24540 dvmptres3 24559 dvlip2 24598 dvgt0lem2 24606 dvne0 24614 rlimcnp2 25552 jensen 25574 eupthvdres 28020 sspg 28511 ssps 28513 sspn 28519 hhsssh 29052 fnresin 30385 padct 30481 ffsrn 30491 resf1o 30492 gsumle 30775 symgcom 30777 cycpmconjvlem 30833 cycpmconjslem1 30846 cnrrext 31361 indf1ofs 31395 eulerpartlemt 31739 subfacp1lem3 32542 subfacp1lem5 32544 cvmliftlem11 32655 poimirlem9 35066 mapfzcons1 39658 eq0rabdioph 39717 eldioph4b 39752 diophren 39754 pwssplit4 40033 dvresntr 42560 sge0split 43048 |
Copyright terms: Public domain | W3C validator |