Theorem mblvol 25485

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  dom cdm 5622   ↾ cres 5624  ‘cfv 6490  vol*covol 25417  volcvol 25418

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-opab 5159  df-xp 5628  df-rel 5629  df-cnv 5630  df-dm 5632  df-rn 5633  df-res 5634  df-iota 6446  df-fv 6498  df-vol 25420

This theorem is referenced by:  volss  25488  volun  25500  volinun  25501  volfiniun  25502  voliunlem3  25507  volsup  25511  iccvolcl  25522  ovolioo  25523  volioo  25524  ioovolcl  25525  uniioovol  25534  uniioombllem4  25541  volcn  25561  volivth  25562  vitalilem4  25566  i1fima2  25634  i1fd  25636  i1f0rn  25637  itg1val2  25639  itg1ge0  25641  itg11  25646  i1fadd  25650  i1fmul  25651  itg1addlem2  25652  itg1addlem4  25654  i1fres  25660  itg10a  25665  itg1ge0a  25666  itg1climres  25669  mbfi1fseqlem4  25673  itg2const2  25696  itg2gt0  25715  itg2cnlem2  25717  ftc1a  25998  ftc1lem4  26000  itgulm  26371  areaf  26925  cntnevol  34334  volmeas  34337  mblfinlem3  37799  mblfinlem4  37800  ismblfin  37801  voliunnfl  37804  volsupnfl  37805  itg2addnclem  37811  itg2addnclem2  37812  itg2gt0cn  37815  ftc1cnnclem  37831  ftc1anclem7  37839  areacirc  37853  arearect  43399  areaquad  43400  vol0  46145  volge0  46147  volsn  46153  volicc  46184  vonvol  46848