MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mblvol Structured version   Unicode version

Theorem mblvol 21138
Description: The volume of a measurable set is the same as its outer volume. (Contributed by Mario Carneiro, 17-Mar-2014.)
Assertion
Ref Expression
mblvol  |-  ( A  e.  dom  vol  ->  ( vol `  A )  =  ( vol* `  A ) )

Proof of Theorem mblvol
StepHypRef Expression
1 volres 21136 . . 3  |-  vol  =  ( vol*  |`  dom  vol )
21fveq1i 5793 . 2  |-  ( vol `  A )  =  ( ( vol*  |`  dom  vol ) `  A )
3 fvres 5806 . 2  |-  ( A  e.  dom  vol  ->  ( ( vol*  |`  dom  vol ) `  A )  =  ( vol* `  A ) )
42, 3syl5eq 2504 1  |-  ( A  e.  dom  vol  ->  ( vol `  A )  =  ( vol* `  A ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1370    e. wcel 1758   dom cdm 4941    |` cres 4943   ` cfv 5519   vol*covol 21071   volcvol 21072
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-sep 4514  ax-nul 4522  ax-pr 4632
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-mo 2265  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-ral 2800  df-rex 2801  df-rab 2804  df-v 3073  df-dif 3432  df-un 3434  df-in 3436  df-ss 3443  df-nul 3739  df-if 3893  df-sn 3979  df-pr 3981  df-op 3985  df-uni 4193  df-br 4394  df-opab 4452  df-xp 4947  df-rel 4948  df-cnv 4949  df-dm 4951  df-rn 4952  df-res 4953  df-iota 5482  df-fv 5527  df-vol 21074
This theorem is referenced by:  volss  21141  volun  21152  volinun  21153  volfiniun  21154  voliunlem3  21159  volsup  21163  iccvolcl  21174  ovolioo  21175  ioovolcl  21176  uniioovol  21185  uniioombllem4  21192  volcn  21212  volivth  21213  vitalilem4  21217  i1fima2  21283  i1fd  21285  i1f0rn  21286  itg1val2  21288  itg1ge0  21290  itg11  21295  i1fadd  21299  i1fmul  21300  itg1addlem2  21301  itg1addlem4  21303  i1fres  21309  itg10a  21314  itg1ge0a  21315  itg1climres  21318  mbfi1fseqlem4  21322  itg2const2  21345  itg2gt0  21364  itg2cnlem2  21366  ftc1a  21635  ftc1lem4  21637  itgulm  21999  areaf  22481  cntnevol  26780  volmeas  26784  mblfinlem3  28571  mblfinlem4  28572  ismblfin  28573  voliunnfl  28576  volsupnfl  28577  itg2addnclem  28584  itg2addnclem2  28585  itg2gt0cn  28588  ftc1cnnclem  28606  ftc1anclem7  28614  areacirc  28630  arearect  29732  areaquad  29733  volioo  29930
  Copyright terms: Public domain W3C validator