Theorem mblvol 25851

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 25849	. . 3 ⊢ vol = (vol* ↾ dom vol)
2	1	fveq1i 6886	. 2 ⊢ (vol‘𝐴) = ((vol* ↾ dom vol)‘𝐴)
3		fvres 6904	. 2 ⊢ (𝐴 ∈ dom vol → ((vol* ↾ dom vol)‘𝐴) = (vol*‘𝐴))
4	2, 3	eqtrid 2808	1 ⊢ (𝐴 ∈ dom vol → (vol‘𝐴) = (vol*‘𝐴))

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  dom cdm 5651   ↾ cres 5653  ‘cfv 6538  vol*covol 25783  volcvol 25784

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-xp 5657  df-rel 5658  df-cnv 5659  df-dm 5661  df-rn 5662  df-res 5663  df-iota 6494  df-fv 6546  df-vol 25786

This theorem is used by:  volss  25854  volun  25866  volinun  25867  volfiniun  25868  voliunlem3  25873  volsup  25877  iccvolcl  25888  ovolioo  25889  volioo  25890  ioovolcl  25891  uniioovol  25900  uniioombllem4  25907  volcn  25927  volivth  25928  vitalilem4  25932  i1fima2  26000  i1fd  26002  i1f0rn  26003  itg1val2  26005  itg1ge0  26007  itg11  26012  i1fadd  26016  i1fmul  26017  itg1addlem2  26018  itg1addlem4  26020  i1fres  26026  itg10a  26031  itg1ge0a  26032  itg1climres  26035  mbfi1fseqlem4  26039  itg2const2  26062  itg2gt0  26081  itg2cnlem2  26083  ftc1a  26357  ftc1lem4  26359  itgulm  26735  areaf  27289  cntnevol  34861  volmeas  34864  mblfinlem3  38577  mblfinlem4  38578  ismblfin  38579  voliunnfl  38582  volsupnfl  38583  itg2addnclem  38589  itg2addnclem2  38590  itg2gt0cn  38593  ftc1cnnclem  38609  ftc1anclem7  38617  areacirc  38631  arearect  44216  areaquad  44217  vol0  46968  volge0  46970  volsn  46976  volicc  47007  vonvol  47671