Theorem mblvol 25429

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

Step	Hyp	Ref	Expression
1		volres 25427	. . 3 ⊢ vol = (vol* ↾ dom vol)
2	1	fveq1i 6823	. 2 ⊢ (vol‘𝐴) = ((vol* ↾ dom vol)‘𝐴)
3		fvres 6841	. 2 ⊢ (𝐴 ∈ dom vol → ((vol* ↾ dom vol)‘𝐴) = (vol*‘𝐴))
4	2, 3	eqtrid 2776	1 ⊢ (𝐴 ∈ dom vol → (vol‘𝐴) = (vol*‘𝐴))

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  dom cdm 5619   ↾ cres 5621  ‘cfv 6482  vol*covol 25361  volcvol 25362

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pr 5371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-xp 5625  df-rel 5626  df-cnv 5627  df-dm 5629  df-rn 5630  df-res 5631  df-iota 6438  df-fv 6490  df-vol 25364

This theorem is referenced by:  volss  25432  volun  25444  volinun  25445  volfiniun  25446  voliunlem3  25451  volsup  25455  iccvolcl  25466  ovolioo  25467  volioo  25468  ioovolcl  25469  uniioovol  25478  uniioombllem4  25485  volcn  25505  volivth  25506  vitalilem4  25510  i1fima2  25578  i1fd  25580  i1f0rn  25581  itg1val2  25583  itg1ge0  25585  itg11  25590  i1fadd  25594  i1fmul  25595  itg1addlem2  25596  itg1addlem4  25598  i1fres  25604  itg10a  25609  itg1ge0a  25610  itg1climres  25613  mbfi1fseqlem4  25617  itg2const2  25640  itg2gt0  25659  itg2cnlem2  25661  ftc1a  25942  ftc1lem4  25944  itgulm  26315  areaf  26869  cntnevol  34201  volmeas  34204  mblfinlem3  37649  mblfinlem4  37650  ismblfin  37651  voliunnfl  37654  volsupnfl  37655  itg2addnclem  37661  itg2addnclem2  37662  itg2gt0cn  37665  ftc1cnnclem  37681  ftc1anclem7  37689  areacirc  37703  arearect  43198  areaquad  43199  vol0  45950  volge0  45952  volsn  45958  volicc  45989  vonvol  46653