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

Theorem mblvol 24123
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 (𝐴 ∈ dom vol → (vol‘𝐴) = (vol*‘𝐴))

Proof of Theorem mblvol
StepHypRef Expression
1 volres 24121 . . 3 vol = (vol* ↾ dom vol)
21fveq1i 6664 . 2 (vol‘𝐴) = ((vol* ↾ dom vol)‘𝐴)
3 fvres 6682 . 2 (𝐴 ∈ dom vol → ((vol* ↾ dom vol)‘𝐴) = (vol*‘𝐴))
42, 3syl5eq 2866 1 (𝐴 ∈ dom vol → (vol‘𝐴) = (vol*‘𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1530  wcel 2107  dom cdm 5548  cres 5550  cfv 6348  vol*covol 24055  volcvol 24056
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791  ax-sep 5194  ax-nul 5201  ax-pr 5320
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ral 3141  df-rex 3142  df-rab 3145  df-v 3495  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4831  df-br 5058  df-opab 5120  df-xp 5554  df-rel 5555  df-cnv 5556  df-dm 5558  df-rn 5559  df-res 5560  df-iota 6307  df-fv 6356  df-vol 24058
This theorem is referenced by:  volss  24126  volun  24138  volinun  24139  volfiniun  24140  voliunlem3  24145  volsup  24149  iccvolcl  24160  ovolioo  24161  volioo  24162  ioovolcl  24163  uniioovol  24172  uniioombllem4  24179  volcn  24199  volivth  24200  vitalilem4  24204  i1fima2  24272  i1fd  24274  i1f0rn  24275  itg1val2  24277  itg1ge0  24279  itg11  24284  i1fadd  24288  i1fmul  24289  itg1addlem2  24290  itg1addlem4  24292  i1fres  24298  itg10a  24303  itg1ge0a  24304  itg1climres  24307  mbfi1fseqlem4  24311  itg2const2  24334  itg2gt0  24353  itg2cnlem2  24355  ftc1a  24626  ftc1lem4  24628  itgulm  24988  areaf  25531  cntnevol  31475  volmeas  31478  mblfinlem3  34918  mblfinlem4  34919  ismblfin  34920  voliunnfl  34923  volsupnfl  34924  itg2addnclem  34930  itg2addnclem2  34931  itg2gt0cn  34934  ftc1cnnclem  34952  ftc1anclem7  34960  areacirc  34974  arearect  39807  areaquad  39808  vol0  42228  volge0  42230  volsn  42236  volicc  42268  vonvol  42929
  Copyright terms: Public domain W3C validator