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 5903 | . 2 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹) | |
2 | fndm 5904 | . . 3 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴) | |
3 | eqimss 3620 | . . 3 ⊢ (dom 𝐹 = 𝐴 → dom 𝐹 ⊆ 𝐴) | |
4 | 2, 3 | syl 17 | . 2 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 ⊆ 𝐴) |
5 | relssres 5357 | . 2 ⊢ ((Rel 𝐹 ∧ dom 𝐹 ⊆ 𝐴) → (𝐹 ↾ 𝐴) = 𝐹) | |
6 | 1, 4, 5 | syl2anc 691 | 1 ⊢ (𝐹 Fn 𝐴 → (𝐹 ↾ 𝐴) = 𝐹) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1475 ⊆ wss 3540 dom cdm 5038 ↾ cres 5040 Rel wrel 5043 Fn wfn 5799 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-sep 4709 ax-nul 4717 ax-pr 4833 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ral 2901 df-rex 2902 df-rab 2905 df-v 3175 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-nul 3875 df-if 4037 df-sn 4126 df-pr 4128 df-op 4132 df-br 4584 df-opab 4644 df-xp 5044 df-rel 5045 df-dm 5048 df-res 5050 df-fun 5806 df-fn 5807 |
This theorem is referenced by: fnima 5923 fresin 5986 resasplit 5987 fresaunres2 5989 fvreseq1 6226 fnsnb 6337 fninfp 6345 fnsnsplit 6355 fsnunfv 6358 fsnunres 6359 fnsuppeq0 7210 mapunen 8014 fnfi 8123 canthp1lem2 9354 fseq1p1m1 12283 facnn 12924 fac0 12925 hashgval 12982 hashinf 12984 rlimres 14137 lo1res 14138 rlimresb 14144 isercolllem2 14244 isercoll 14246 ruclem4 14802 fsets 15723 sscres 16306 sscid 16307 gsumzres 18133 pwssplit1 18880 zzngim 19720 ptuncnv 21420 ptcmpfi 21426 tsmsres 21757 imasdsf1olem 21988 tmslem 22097 tmsxms 22101 imasf1oxms 22104 prdsxms 22145 tmsxps 22151 tmsxpsmopn 22152 isngp2 22211 tngngp2 22266 cnfldms 22389 cncms 22959 cnfldcusp 22961 mbfres2 23218 dvres 23481 dvres3a 23484 cpnres 23506 dvmptres3 23525 dvlip2 23562 dvgt0lem2 23570 dvne0 23578 rlimcnp2 24493 jensen 24515 eupath2 26507 sspg 26967 ssps 26969 sspn 26975 hhsssh 27510 fnresin 28812 padct 28885 ffsrn 28892 resf1o 28893 gsumle 29110 cnrrext 29382 indf1ofs 29415 eulerpartlemt 29760 bnj142OLD 30048 subfacp1lem3 30418 subfacp1lem5 30420 cvmliftlem11 30531 poimirlem9 32588 mapfzcons1 36298 eq0rabdioph 36358 eldioph4b 36393 diophren 36395 pwssplit4 36677 dvresntr 38806 sge0split 39302 eupthvdres 41403 |
Copyright terms: Public domain | W3C validator |