Theorem mblvol 25565

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 25563	. . 3 ⊢ vol = (vol* ↾ dom vol)
2	1	fveq1i 6907	. 2 ⊢ (vol‘𝐴) = ((vol* ↾ dom vol)‘𝐴)
3		fvres 6925	. 2 ⊢ (𝐴 ∈ dom vol → ((vol* ↾ dom vol)‘𝐴) = (vol*‘𝐴))
4	2, 3	eqtrid 2789	1 ⊢ (𝐴 ∈ dom vol → (vol‘𝐴) = (vol*‘𝐴))

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  dom cdm 5685   ↾ cres 5687  ‘cfv 6561  vol*covol 25497  volcvol 25498

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-xp 5691  df-rel 5692  df-cnv 5693  df-dm 5695  df-rn 5696  df-res 5697  df-iota 6514  df-fv 6569  df-vol 25500

This theorem is referenced by:  volss  25568  volun  25580  volinun  25581  volfiniun  25582  voliunlem3  25587  volsup  25591  iccvolcl  25602  ovolioo  25603  volioo  25604  ioovolcl  25605  uniioovol  25614  uniioombllem4  25621  volcn  25641  volivth  25642  vitalilem4  25646  i1fima2  25714  i1fd  25716  i1f0rn  25717  itg1val2  25719  itg1ge0  25721  itg11  25726  i1fadd  25730  i1fmul  25731  itg1addlem2  25732  itg1addlem4  25734  i1fres  25740  itg10a  25745  itg1ge0a  25746  itg1climres  25749  mbfi1fseqlem4  25753  itg2const2  25776  itg2gt0  25795  itg2cnlem2  25797  ftc1a  26078  ftc1lem4  26080  itgulm  26451  areaf  27004  cntnevol  34229  volmeas  34232  mblfinlem3  37666  mblfinlem4  37667  ismblfin  37668  voliunnfl  37671  volsupnfl  37672  itg2addnclem  37678  itg2addnclem2  37679  itg2gt0cn  37682  ftc1cnnclem  37698  ftc1anclem7  37706  areacirc  37720  arearect  43227  areaquad  43228  vol0  45974  volge0  45976  volsn  45982  volicc  46013  vonvol  46677