Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > mblvol | Structured version Visualization version GIF version |
Description: The volume of a measurable set is the same as its outer volume. (Contributed by Mario Carneiro, 17-Mar-2014.) |
Ref | Expression |
---|---|
mblvol | ⊢ (𝐴 ∈ dom vol → (vol‘𝐴) = (vol*‘𝐴)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | volres 24131 | . . 3 ⊢ vol = (vol* ↾ dom vol) | |
2 | 1 | fveq1i 6673 | . 2 ⊢ (vol‘𝐴) = ((vol* ↾ dom vol)‘𝐴) |
3 | fvres 6691 | . 2 ⊢ (𝐴 ∈ dom vol → ((vol* ↾ dom vol)‘𝐴) = (vol*‘𝐴)) | |
4 | 2, 3 | syl5eq 2870 | 1 ⊢ (𝐴 ∈ dom vol → (vol‘𝐴) = (vol*‘𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1537 ∈ wcel 2114 dom cdm 5557 ↾ cres 5559 ‘cfv 6357 vol*covol 24065 volcvol 24066 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2795 ax-sep 5205 ax-nul 5212 ax-pr 5332 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2802 df-cleq 2816 df-clel 2895 df-nfc 2965 df-ral 3145 df-rex 3146 df-rab 3149 df-v 3498 df-dif 3941 df-un 3943 df-in 3945 df-ss 3954 df-nul 4294 df-if 4470 df-sn 4570 df-pr 4572 df-op 4576 df-uni 4841 df-br 5069 df-opab 5131 df-xp 5563 df-rel 5564 df-cnv 5565 df-dm 5567 df-rn 5568 df-res 5569 df-iota 6316 df-fv 6365 df-vol 24068 |
This theorem is referenced by: volss 24136 volun 24148 volinun 24149 volfiniun 24150 voliunlem3 24155 volsup 24159 iccvolcl 24170 ovolioo 24171 volioo 24172 ioovolcl 24173 uniioovol 24182 uniioombllem4 24189 volcn 24209 volivth 24210 vitalilem4 24214 i1fima2 24282 i1fd 24284 i1f0rn 24285 itg1val2 24287 itg1ge0 24289 itg11 24294 i1fadd 24298 i1fmul 24299 itg1addlem2 24300 itg1addlem4 24302 i1fres 24308 itg10a 24313 itg1ge0a 24314 itg1climres 24317 mbfi1fseqlem4 24321 itg2const2 24344 itg2gt0 24363 itg2cnlem2 24365 ftc1a 24636 ftc1lem4 24638 itgulm 24998 areaf 25541 cntnevol 31489 volmeas 31492 mblfinlem3 34933 mblfinlem4 34934 ismblfin 34935 voliunnfl 34938 volsupnfl 34939 itg2addnclem 34945 itg2addnclem2 34946 itg2gt0cn 34949 ftc1cnnclem 34967 ftc1anclem7 34975 areacirc 34989 arearect 39829 areaquad 39830 vol0 42251 volge0 42253 volsn 42259 volicc 42290 vonvol 42951 |
Copyright terms: Public domain | W3C validator |