Theorem mblvol 24599

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 24597	. . 3 ⊢ vol = (vol* ↾ dom vol)
2	1	fveq1i 6757	. 2 ⊢ (vol‘𝐴) = ((vol* ↾ dom vol)‘𝐴)
3		fvres 6775	. 2 ⊢ (𝐴 ∈ dom vol → ((vol* ↾ dom vol)‘𝐴) = (vol*‘𝐴))
4	2, 3	syl5eq 2791	1 ⊢ (𝐴 ∈ dom vol → (vol‘𝐴) = (vol*‘𝐴))

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2108  dom cdm 5580   ↾ cres 5582  ‘cfv 6418  vol*covol 24531  volcvol 24532

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-xp 5586  df-rel 5587  df-cnv 5588  df-dm 5590  df-rn 5591  df-res 5592  df-iota 6376  df-fv 6426  df-vol 24534

This theorem is referenced by:  volss  24602  volun  24614  volinun  24615  volfiniun  24616  voliunlem3  24621  volsup  24625  iccvolcl  24636  ovolioo  24637  volioo  24638  ioovolcl  24639  uniioovol  24648  uniioombllem4  24655  volcn  24675  volivth  24676  vitalilem4  24680  i1fima2  24748  i1fd  24750  i1f0rn  24751  itg1val2  24753  itg1ge0  24755  itg11  24760  i1fadd  24764  i1fmul  24765  itg1addlem2  24766  itg1addlem4  24768  itg1addlem4OLD  24769  i1fres  24775  itg10a  24780  itg1ge0a  24781  itg1climres  24784  mbfi1fseqlem4  24788  itg2const2  24811  itg2gt0  24830  itg2cnlem2  24832  ftc1a  25106  ftc1lem4  25108  itgulm  25472  areaf  26016  cntnevol  32096  volmeas  32099  mblfinlem3  35743  mblfinlem4  35744  ismblfin  35745  voliunnfl  35748  volsupnfl  35749  itg2addnclem  35755  itg2addnclem2  35756  itg2gt0cn  35759  ftc1cnnclem  35775  ftc1anclem7  35783  areacirc  35797  arearect  40962  areaquad  40963  vol0  43390  volge0  43392  volsn  43398  volicc  43429  vonvol  44090