Theorem mblvol 25510

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 25508	. . 3 ⊢ vol = (vol* ↾ dom vol)
2	1	fveq1i 6836	. 2 ⊢ (vol‘𝐴) = ((vol* ↾ dom vol)‘𝐴)
3		fvres 6854	. 2 ⊢ (𝐴 ∈ dom vol → ((vol* ↾ dom vol)‘𝐴) = (vol*‘𝐴))
4	2, 3	eqtrid 2784	1 ⊢ (𝐴 ∈ dom vol → (vol‘𝐴) = (vol*‘𝐴))

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  dom cdm 5625   ↾ cres 5627  ‘cfv 6493  vol*covol 25442  volcvol 25443

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5232  ax-pr 5371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-xp 5631  df-rel 5632  df-cnv 5633  df-dm 5635  df-rn 5636  df-res 5637  df-iota 6449  df-fv 6501  df-vol 25445

This theorem is referenced by:  volss  25513  volun  25525  volinun  25526  volfiniun  25527  voliunlem3  25532  volsup  25536  iccvolcl  25547  ovolioo  25548  volioo  25549  ioovolcl  25550  uniioovol  25559  uniioombllem4  25566  volcn  25586  volivth  25587  vitalilem4  25591  i1fima2  25659  i1fd  25661  i1f0rn  25662  itg1val2  25664  itg1ge0  25666  itg11  25671  i1fadd  25675  i1fmul  25676  itg1addlem2  25677  itg1addlem4  25679  i1fres  25685  itg10a  25690  itg1ge0a  25691  itg1climres  25694  mbfi1fseqlem4  25698  itg2const2  25721  itg2gt0  25740  itg2cnlem2  25742  ftc1a  26017  ftc1lem4  26019  itgulm  26389  areaf  26941  cntnevol  34391  volmeas  34394  mblfinlem3  37997  mblfinlem4  37998  ismblfin  37999  voliunnfl  38002  volsupnfl  38003  itg2addnclem  38009  itg2addnclem2  38010  itg2gt0cn  38013  ftc1cnnclem  38029  ftc1anclem7  38037  areacirc  38051  arearect  43664  areaquad  43665  vol0  46408  volge0  46410  volsn  46416  volicc  46447  vonvol  47111