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 6448 | . 2 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹) | |
2 | fndm 6449 | . . 3 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴) | |
3 | eqimss 4022 | . . 3 ⊢ (dom 𝐹 = 𝐴 → dom 𝐹 ⊆ 𝐴) | |
4 | 2, 3 | syl 17 | . 2 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 ⊆ 𝐴) |
5 | relssres 5887 | . 2 ⊢ ((Rel 𝐹 ∧ dom 𝐹 ⊆ 𝐴) → (𝐹 ↾ 𝐴) = 𝐹) | |
6 | 1, 4, 5 | syl2anc 584 | 1 ⊢ (𝐹 Fn 𝐴 → (𝐹 ↾ 𝐴) = 𝐹) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1528 ⊆ wss 3935 dom cdm 5549 ↾ cres 5551 Rel wrel 5554 Fn wfn 6344 |
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 2793 ax-sep 5195 ax-nul 5202 ax-pr 5321 |
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 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ral 3143 df-rex 3144 df-rab 3147 df-v 3497 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-nul 4291 df-if 4466 df-sn 4560 df-pr 4562 df-op 4566 df-br 5059 df-opab 5121 df-xp 5555 df-rel 5556 df-dm 5559 df-res 5561 df-fun 6351 df-fn 6352 |
This theorem is referenced by: fnima 6472 fresin 6541 resasplit 6542 fresaunres2 6544 fvreseq1 6802 fnsnr 6920 fninfp 6929 fnsnsplit 6939 fsnunfv 6942 fsnunres 6943 fnsuppeq0 7849 mapunen 8675 fnfi 8785 canthp1lem2 10064 fseq1p1m1 12971 facnn 13625 fac0 13626 hashgval 13683 hashinf 13685 rlimres 14905 lo1res 14906 rlimresb 14912 isercolllem2 15012 isercoll 15014 ruclem4 15577 fsets 16506 sscres 17083 sscid 17084 gsumzres 18960 rnrhmsubrg 19498 pwssplit1 19762 zzngim 20629 ptuncnv 22345 ptcmpfi 22351 tsmsres 22681 imasdsf1olem 22912 tmslem 23021 tmsxms 23025 imasf1oxms 23028 prdsxms 23069 tmsxps 23075 tmsxpsmopn 23076 isngp2 23135 tngngp2 23190 cnfldms 23313 cncms 23887 cnfldcusp 23889 mbfres2 24175 dvres 24438 dvres3a 24441 cpnres 24463 dvmptres3 24482 dvlip2 24521 dvgt0lem2 24529 dvne0 24537 rlimcnp2 25472 jensen 25494 eupthvdres 27942 sspg 28433 ssps 28435 sspn 28441 hhsssh 28974 fnresin 30300 padct 30382 ffsrn 30392 resf1o 30393 gsumle 30653 symgcom 30655 cycpmconjvlem 30711 cycpmconjslem1 30724 cnrrext 31151 indf1ofs 31185 eulerpartlemt 31529 subfacp1lem3 32327 subfacp1lem5 32329 cvmliftlem11 32440 poimirlem9 34783 mapfzcons1 39194 eq0rabdioph 39253 eldioph4b 39288 diophren 39290 pwssplit4 39569 dvresntr 42082 sge0split 42572 |
Copyright terms: Public domain | W3C validator |