Theorem mblvol 25501

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 25499	. . 3 ⊢ vol = (vol* ↾ dom vol)
2	1	fveq1i 6887	. 2 ⊢ (vol‘𝐴) = ((vol* ↾ dom vol)‘𝐴)
3		fvres 6905	. 2 ⊢ (𝐴 ∈ dom vol → ((vol* ↾ dom vol)‘𝐴) = (vol*‘𝐴))
4	2, 3	eqtrid 2781	1 ⊢ (𝐴 ∈ dom vol → (vol‘𝐴) = (vol*‘𝐴))

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2107  dom cdm 5665   ↾ cres 5667  ‘cfv 6541  vol*covol 25433  volcvol 25434

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706  ax-sep 5276  ax-nul 5286  ax-pr 5412

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-ral 3051  df-rex 3060  df-rab 3420  df-v 3465  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4888  df-br 5124  df-opab 5186  df-xp 5671  df-rel 5672  df-cnv 5673  df-dm 5675  df-rn 5676  df-res 5677  df-iota 6494  df-fv 6549  df-vol 25436

This theorem is referenced by:  volss  25504  volun  25516  volinun  25517  volfiniun  25518  voliunlem3  25523  volsup  25527  iccvolcl  25538  ovolioo  25539  volioo  25540  ioovolcl  25541  uniioovol  25550  uniioombllem4  25557  volcn  25577  volivth  25578  vitalilem4  25582  i1fima2  25650  i1fd  25652  i1f0rn  25653  itg1val2  25655  itg1ge0  25657  itg11  25662  i1fadd  25666  i1fmul  25667  itg1addlem2  25668  itg1addlem4  25670  i1fres  25676  itg10a  25681  itg1ge0a  25682  itg1climres  25685  mbfi1fseqlem4  25689  itg2const2  25712  itg2gt0  25731  itg2cnlem2  25733  ftc1a  26014  ftc1lem4  26016  itgulm  26387  areaf  26940  cntnevol  34188  volmeas  34191  mblfinlem3  37625  mblfinlem4  37626  ismblfin  37627  voliunnfl  37630  volsupnfl  37631  itg2addnclem  37637  itg2addnclem2  37638  itg2gt0cn  37641  ftc1cnnclem  37657  ftc1anclem7  37665  areacirc  37679  arearect  43190  areaquad  43191  vol0  45931  volge0  45933  volsn  45939  volicc  45970  vonvol  46634