Theorem mblvol 25464

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 25462	. . 3 ⊢ vol = (vol* ↾ dom vol)
2	1	fveq1i 6841	. 2 ⊢ (vol‘𝐴) = ((vol* ↾ dom vol)‘𝐴)
3		fvres 6859	. 2 ⊢ (𝐴 ∈ dom vol → ((vol* ↾ dom vol)‘𝐴) = (vol*‘𝐴))
4	2, 3	eqtrid 2776	1 ⊢ (𝐴 ∈ dom vol → (vol‘𝐴) = (vol*‘𝐴))

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  dom cdm 5631   ↾ cres 5633  ‘cfv 6499  vol*covol 25396  volcvol 25397

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382

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 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-xp 5637  df-rel 5638  df-cnv 5639  df-dm 5641  df-rn 5642  df-res 5643  df-iota 6452  df-fv 6507  df-vol 25399

This theorem is referenced by:  volss  25467  volun  25479  volinun  25480  volfiniun  25481  voliunlem3  25486  volsup  25490  iccvolcl  25501  ovolioo  25502  volioo  25503  ioovolcl  25504  uniioovol  25513  uniioombllem4  25520  volcn  25540  volivth  25541  vitalilem4  25545  i1fima2  25613  i1fd  25615  i1f0rn  25616  itg1val2  25618  itg1ge0  25620  itg11  25625  i1fadd  25629  i1fmul  25630  itg1addlem2  25631  itg1addlem4  25633  i1fres  25639  itg10a  25644  itg1ge0a  25645  itg1climres  25648  mbfi1fseqlem4  25652  itg2const2  25675  itg2gt0  25694  itg2cnlem2  25696  ftc1a  25977  ftc1lem4  25979  itgulm  26350  areaf  26904  cntnevol  34211  volmeas  34214  mblfinlem3  37646  mblfinlem4  37647  ismblfin  37648  voliunnfl  37651  volsupnfl  37652  itg2addnclem  37658  itg2addnclem2  37659  itg2gt0cn  37662  ftc1cnnclem  37678  ftc1anclem7  37686  areacirc  37700  arearect  43197  areaquad  43198  vol0  45950  volge0  45952  volsn  45958  volicc  45989  vonvol  46653