Theorem mblvol 25592

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 25590	. . 3 ⊢ vol = (vol* ↾ dom vol)
2	1	fveq1i 6868	. 2 ⊢ (vol‘𝐴) = ((vol* ↾ dom vol)‘𝐴)
3		fvres 6886	. 2 ⊢ (𝐴 ∈ dom vol → ((vol* ↾ dom vol)‘𝐴) = (vol*‘𝐴))
4	2, 3	eqtrid 2809	1 ⊢ (𝐴 ∈ dom vol → (vol‘𝐴) = (vol*‘𝐴))

Syntax hints:   → wi 4   = wceq 1560   ∈ wcel 2142  dom cdm 5647   ↾ cres 5649  ‘cfv 6521  vol*covol 25524  volcvol 25525

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734  ax-sep 5246  ax-pr 5390

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3077  df-rex 3087  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-xp 5653  df-rel 5654  df-cnv 5655  df-dm 5657  df-rn 5658  df-res 5659  df-iota 6477  df-fv 6529  df-vol 25527

This theorem is referenced by:  volss  25595  volun  25607  volinun  25608  volfiniun  25609  voliunlem3  25614  volsup  25618  iccvolcl  25629  ovolioo  25630  volioo  25631  ioovolcl  25632  uniioovol  25641  uniioombllem4  25648  volcn  25668  volivth  25669  vitalilem4  25673  i1fima2  25741  i1fd  25743  i1f0rn  25744  itg1val2  25746  itg1ge0  25748  itg11  25753  i1fadd  25757  i1fmul  25758  itg1addlem2  25759  itg1addlem4  25761  i1fres  25767  itg10a  25772  itg1ge0a  25773  itg1climres  25776  mbfi1fseqlem4  25780  itg2const2  25803  itg2gt0  25822  itg2cnlem2  25824  ftc1a  26099  ftc1lem4  26101  itgulm  26471  areaf  27026  cntnevol  34525  volmeas  34528  mblfinlem3  38158  mblfinlem4  38159  ismblfin  38160  voliunnfl  38163  volsupnfl  38164  itg2addnclem  38170  itg2addnclem2  38171  itg2gt0cn  38174  ftc1cnnclem  38190  ftc1anclem7  38198  areacirc  38212  arearect  43792  areaquad  43793  vol0  46533  volge0  46535  volsn  46541  volicc  46572  vonvol  47236