Theorem mblvol 20988

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 20986	. . 3 |- vol = ( vol* |` dom vol )
2	1	fveq1i 5687	. 2 |- ( vol ` A ) = ( ( vol* |` dom vol ) ` A )
3		fvres 5699	. 2 |- ( A e. dom vol -> ( ( vol* |` dom vol ) ` A ) = ( vol* ` A ) )
4	2, 3	syl5eq 2482	1 |- ( A e. dom vol -> ( vol ` A ) = ( vol* ` A ) )

Syntax hints:   -> wi 4   = wceq 1369   e. wcel 1756   dom cdm 4835   |` cres 4837   ` cfv 5413   vol*covol 20921   volcvol 20922

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-sep 4408  ax-nul 4416  ax-pr 4526

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2715  df-rex 2716  df-rab 2719  df-v 2969  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-br 4288  df-opab 4346  df-xp 4841  df-rel 4842  df-cnv 4843  df-dm 4845  df-rn 4846  df-res 4847  df-iota 5376  df-fv 5421  df-vol 20924

This theorem is referenced by:  volun  21001  volinun  21002  volfiniun  21003  voliunlem3  21008  volsup  21012  iccvolcl  21023  ovolioo  21024  ioovolcl  21025  uniioovol  21034  uniioombllem4  21041  volcn  21061  volivth  21062  vitalilem4  21066  i1fima2  21132  i1fd  21134  i1f0rn  21135  itg1val2  21137  itg1ge0  21139  itg11  21144  i1fadd  21148  i1fmul  21149  itg1addlem2  21150  itg1addlem4  21152  i1fres  21158  itg10a  21163  itg1ge0a  21164  itg1climres  21167  mbfi1fseqlem4  21171  itg2const2  21194  itg2gt0  21213  itg2cnlem2  21215  ftc1a  21484  ftc1lem4  21486  itgulm  21848  areaf  22330  cntnevol  26594  volss  26595  volmeas  26599  mblfinlem3  28383  mblfinlem4  28384  ismblfin  28385  voliunnfl  28388  volsupnfl  28389  itg2addnclem  28396  itg2addnclem2  28397  itg2gt0cn  28400  ftc1cnnclem  28418  ftc1anclem7  28426  areacirc  28442  arearect  29544  areaquad  29545  volioo  29742