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

Theorem mblvol 24897
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 24895 . . 3 vol = (vol* ↾ dom vol)
21fveq1i 6844 . 2 (vol‘𝐴) = ((vol* ↾ dom vol)‘𝐴)
3 fvres 6862 . 2 (𝐴 ∈ dom vol → ((vol* ↾ dom vol)‘𝐴) = (vol*‘𝐴))
42, 3eqtrid 2789 1 (𝐴 ∈ dom vol → (vol‘𝐴) = (vol*‘𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  wcel 2107  dom cdm 5634  cres 5636  cfv 6497  vol*covol 24829  volcvol 24830
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-12 2172  ax-ext 2708  ax-sep 5257  ax-nul 5264  ax-pr 5385
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-ral 3066  df-rex 3075  df-rab 3409  df-v 3448  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-opab 5169  df-xp 5640  df-rel 5641  df-cnv 5642  df-dm 5644  df-rn 5645  df-res 5646  df-iota 6449  df-fv 6505  df-vol 24832
This theorem is referenced by:  volss  24900  volun  24912  volinun  24913  volfiniun  24914  voliunlem3  24919  volsup  24923  iccvolcl  24934  ovolioo  24935  volioo  24936  ioovolcl  24937  uniioovol  24946  uniioombllem4  24953  volcn  24973  volivth  24974  vitalilem4  24978  i1fima2  25046  i1fd  25048  i1f0rn  25049  itg1val2  25051  itg1ge0  25053  itg11  25058  i1fadd  25062  i1fmul  25063  itg1addlem2  25064  itg1addlem4  25066  itg1addlem4OLD  25067  i1fres  25073  itg10a  25078  itg1ge0a  25079  itg1climres  25082  mbfi1fseqlem4  25086  itg2const2  25109  itg2gt0  25128  itg2cnlem2  25130  ftc1a  25404  ftc1lem4  25406  itgulm  25770  areaf  26314  cntnevol  32830  volmeas  32833  mblfinlem3  36120  mblfinlem4  36121  ismblfin  36122  voliunnfl  36125  volsupnfl  36126  itg2addnclem  36132  itg2addnclem2  36133  itg2gt0cn  36136  ftc1cnnclem  36152  ftc1anclem7  36160  areacirc  36174  arearect  41552  areaquad  41553  vol0  44207  volge0  44209  volsn  44215  volicc  44246  vonvol  44910
  Copyright terms: Public domain W3C validator