Theorem mblvol 21807

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 21805	. . 3 |- vol = ( vol* |` dom vol )
2	1	fveq1i 5853	. 2 |- ( vol ` A ) = ( ( vol* |` dom vol ) ` A )
3		fvres 5866	. 2 |- ( A e. dom vol -> ( ( vol* |` dom vol ) ` A ) = ( vol* ` A ) )
4	2, 3	syl5eq 2494	1 |- ( A e. dom vol -> ( vol ` A ) = ( vol* ` A ) )

Syntax hints:   -> wi 4   = wceq 1381   e. wcel 1802   dom cdm 4985   |` cres 4987   ` cfv 5574   vol*covol 21740   volcvol 21741

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-9 1806  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-sep 4554  ax-nul 4562  ax-pr 4672

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-eu 2270  df-mo 2271  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-ral 2796  df-rex 2797  df-rab 2800  df-v 3095  df-dif 3461  df-un 3463  df-in 3465  df-ss 3472  df-nul 3768  df-if 3923  df-sn 4011  df-pr 4013  df-op 4017  df-uni 4231  df-br 4434  df-opab 4492  df-xp 4991  df-rel 4992  df-cnv 4993  df-dm 4995  df-rn 4996  df-res 4997  df-iota 5537  df-fv 5582  df-vol 21743

This theorem is referenced by:  volss  21810  volun  21821  volinun  21822  volfiniun  21823  voliunlem3  21828  volsup  21832  iccvolcl  21843  ovolioo  21844  ioovolcl  21845  uniioovol  21854  uniioombllem4  21861  volcn  21881  volivth  21882  vitalilem4  21886  i1fima2  21952  i1fd  21954  i1f0rn  21955  itg1val2  21957  itg1ge0  21959  itg11  21964  i1fadd  21968  i1fmul  21969  itg1addlem2  21970  itg1addlem4  21972  i1fres  21978  itg10a  21983  itg1ge0a  21984  itg1climres  21987  mbfi1fseqlem4  21991  itg2const2  22014  itg2gt0  22033  itg2cnlem2  22035  ftc1a  22304  ftc1lem4  22306  itgulm  22668  areaf  23156  cntnevol  28065  volmeas  28069  mblfinlem3  30021  mblfinlem4  30022  ismblfin  30023  voliunnfl  30026  volsupnfl  30027  itg2addnclem  30034  itg2addnclem2  30035  itg2gt0cn  30038  ftc1cnnclem  30056  ftc1anclem7  30064  areacirc  30080  arearect  31152  areaquad  31153  volioo  31633  vol0  31644  volge0  31646  volsn  31652