![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > mblvol | Structured version Visualization version Unicode 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 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | volres 22530 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | fveq1i 5888 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | fvres 5901 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | syl5eq 2507 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1679 ax-4 1692 ax-5 1768 ax-6 1815 ax-7 1861 ax-9 1906 ax-10 1925 ax-11 1930 ax-12 1943 ax-13 2101 ax-ext 2441 ax-sep 4538 ax-nul 4547 ax-pr 4652 |
This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3an 993 df-tru 1457 df-ex 1674 df-nf 1678 df-sb 1808 df-eu 2313 df-mo 2314 df-clab 2448 df-cleq 2454 df-clel 2457 df-nfc 2591 df-ne 2634 df-ral 2753 df-rex 2754 df-rab 2757 df-v 3058 df-dif 3418 df-un 3420 df-in 3422 df-ss 3429 df-nul 3743 df-if 3893 df-sn 3980 df-pr 3982 df-op 3986 df-uni 4212 df-br 4416 df-opab 4475 df-xp 4858 df-rel 4859 df-cnv 4860 df-dm 4862 df-rn 4863 df-res 4864 df-iota 5564 df-fv 5608 df-vol 22466 |
This theorem is referenced by: volss 22535 volun 22546 volinun 22547 volfiniun 22548 voliunlem3 22553 volsup 22557 iccvolcl 22568 ovolioo 22569 ioovolcl 22570 uniioovol 22584 uniioombllem4 22592 volcn 22612 volivth 22613 vitalilem4 22617 i1fima2 22685 i1fd 22687 i1f0rn 22688 itg1val2 22690 itg1ge0 22692 itg11 22697 i1fadd 22701 i1fmul 22702 itg1addlem2 22703 itg1addlem4 22705 i1fres 22711 itg10a 22716 itg1ge0a 22717 itg1climres 22720 mbfi1fseqlem4 22724 itg2const2 22747 itg2gt0 22766 itg2cnlem2 22768 ftc1a 23037 ftc1lem4 23039 itgulm 23411 areaf 23935 cntnevol 29098 volmeas 29102 mblfinlem3 32023 mblfinlem4 32024 ismblfin 32025 voliunnfl 32028 volsupnfl 32029 itg2addnclem 32037 itg2addnclem2 32038 itg2gt0cn 32041 ftc1cnnclem 32059 ftc1anclem7 32067 areacirc 32081 arearect 36144 areaquad 36145 volioo 37862 vol0 37873 volge0 37875 volsn 37881 |
Copyright terms: Public domain | W3C validator |