Theorem mblvol 25483

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 25481	. . 3 ⊢ vol = (vol* ↾ dom vol)
2	1	fveq1i 6877	. 2 ⊢ (vol‘𝐴) = ((vol* ↾ dom vol)‘𝐴)
3		fvres 6895	. 2 ⊢ (𝐴 ∈ dom vol → ((vol* ↾ dom vol)‘𝐴) = (vol*‘𝐴))
4	2, 3	eqtrid 2782	1 ⊢ (𝐴 ∈ dom vol → (vol‘𝐴) = (vol*‘𝐴))

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  dom cdm 5654   ↾ cres 5656  ‘cfv 6531  vol*covol 25415  volcvol 25416

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 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-xp 5660  df-rel 5661  df-cnv 5662  df-dm 5664  df-rn 5665  df-res 5666  df-iota 6484  df-fv 6539  df-vol 25418

This theorem is referenced by:  volss  25486  volun  25498  volinun  25499  volfiniun  25500  voliunlem3  25505  volsup  25509  iccvolcl  25520  ovolioo  25521  volioo  25522  ioovolcl  25523  uniioovol  25532  uniioombllem4  25539  volcn  25559  volivth  25560  vitalilem4  25564  i1fima2  25632  i1fd  25634  i1f0rn  25635  itg1val2  25637  itg1ge0  25639  itg11  25644  i1fadd  25648  i1fmul  25649  itg1addlem2  25650  itg1addlem4  25652  i1fres  25658  itg10a  25663  itg1ge0a  25664  itg1climres  25667  mbfi1fseqlem4  25671  itg2const2  25694  itg2gt0  25713  itg2cnlem2  25715  ftc1a  25996  ftc1lem4  25998  itgulm  26369  areaf  26923  cntnevol  34259  volmeas  34262  mblfinlem3  37683  mblfinlem4  37684  ismblfin  37685  voliunnfl  37688  volsupnfl  37689  itg2addnclem  37695  itg2addnclem2  37696  itg2gt0cn  37699  ftc1cnnclem  37715  ftc1anclem7  37723  areacirc  37737  arearect  43239  areaquad  43240  vol0  45988  volge0  45990  volsn  45996  volicc  46027  vonvol  46691