Theorem mblvol 25579

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 25577	. . 3 ⊢ vol = (vol* ↾ dom vol)
2	1	fveq1i 6908	. 2 ⊢ (vol‘𝐴) = ((vol* ↾ dom vol)‘𝐴)
3		fvres 6926	. 2 ⊢ (𝐴 ∈ dom vol → ((vol* ↾ dom vol)‘𝐴) = (vol*‘𝐴))
4	2, 3	eqtrid 2787	1 ⊢ (𝐴 ∈ dom vol → (vol‘𝐴) = (vol*‘𝐴))

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2106  dom cdm 5689   ↾ cres 5691  ‘cfv 6563  vol*covol 25511  volcvol 25512

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-xp 5695  df-rel 5696  df-cnv 5697  df-dm 5699  df-rn 5700  df-res 5701  df-iota 6516  df-fv 6571  df-vol 25514

This theorem is referenced by:  volss  25582  volun  25594  volinun  25595  volfiniun  25596  voliunlem3  25601  volsup  25605  iccvolcl  25616  ovolioo  25617  volioo  25618  ioovolcl  25619  uniioovol  25628  uniioombllem4  25635  volcn  25655  volivth  25656  vitalilem4  25660  i1fima2  25728  i1fd  25730  i1f0rn  25731  itg1val2  25733  itg1ge0  25735  itg11  25740  i1fadd  25744  i1fmul  25745  itg1addlem2  25746  itg1addlem4  25748  itg1addlem4OLD  25749  i1fres  25755  itg10a  25760  itg1ge0a  25761  itg1climres  25764  mbfi1fseqlem4  25768  itg2const2  25791  itg2gt0  25810  itg2cnlem2  25812  ftc1a  26093  ftc1lem4  26095  itgulm  26466  areaf  27019  cntnevol  34209  volmeas  34212  mblfinlem3  37646  mblfinlem4  37647  ismblfin  37648  voliunnfl  37651  volsupnfl  37652  itg2addnclem  37658  itg2addnclem2  37659  itg2gt0cn  37662  ftc1cnnclem  37678  ftc1anclem7  37686  areacirc  37700  arearect  43204  areaquad  43205  vol0  45915  volge0  45917  volsn  45923  volicc  45954  vonvol  46618