Theorem mblvol 25487

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 25485	. . 3 ⊢ vol = (vol* ↾ dom vol)
2	1	fveq1i 6835	. 2 ⊢ (vol‘𝐴) = ((vol* ↾ dom vol)‘𝐴)
3		fvres 6853	. 2 ⊢ (𝐴 ∈ dom vol → ((vol* ↾ dom vol)‘𝐴) = (vol*‘𝐴))
4	2, 3	eqtrid 2783	1 ⊢ (𝐴 ∈ dom vol → (vol‘𝐴) = (vol*‘𝐴))

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  dom cdm 5624   ↾ cres 5626  ‘cfv 6492  vol*covol 25419  volcvol 25420

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 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

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 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-xp 5630  df-rel 5631  df-cnv 5632  df-dm 5634  df-rn 5635  df-res 5636  df-iota 6448  df-fv 6500  df-vol 25422

This theorem is referenced by:  volss  25490  volun  25502  volinun  25503  volfiniun  25504  voliunlem3  25509  volsup  25513  iccvolcl  25524  ovolioo  25525  volioo  25526  ioovolcl  25527  uniioovol  25536  uniioombllem4  25543  volcn  25563  volivth  25564  vitalilem4  25568  i1fima2  25636  i1fd  25638  i1f0rn  25639  itg1val2  25641  itg1ge0  25643  itg11  25648  i1fadd  25652  i1fmul  25653  itg1addlem2  25654  itg1addlem4  25656  i1fres  25662  itg10a  25667  itg1ge0a  25668  itg1climres  25671  mbfi1fseqlem4  25675  itg2const2  25698  itg2gt0  25717  itg2cnlem2  25719  ftc1a  26000  ftc1lem4  26002  itgulm  26373  areaf  26927  cntnevol  34385  volmeas  34388  mblfinlem3  37860  mblfinlem4  37861  ismblfin  37862  voliunnfl  37865  volsupnfl  37866  itg2addnclem  37872  itg2addnclem2  37873  itg2gt0cn  37876  ftc1cnnclem  37892  ftc1anclem7  37900  areacirc  37914  arearect  43467  areaquad  43468  vol0  46213  volge0  46215  volsn  46221  volicc  46252  vonvol  46916