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

Step	Hyp	Ref	Expression
1		volres 21136	. . 3 |- vol = ( vol* |` dom vol )
2	1	fveq1i 5793	. 2 |- ( vol ` A ) = ( ( vol* |` dom vol ) ` A )
3		fvres 5806	. 2 |- ( A e. dom vol -> ( ( vol* |` dom vol ) ` A ) = ( vol* ` A ) )
4	2, 3	syl5eq 2504	1 |- ( A e. dom vol -> ( vol ` A ) = ( vol* ` A ) )

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