Theorem mblvol 25689

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 25687	. . 3 ⊢ vol = (vol* ↾ dom vol)
2	1	fveq1i 6882	. 2 ⊢ (vol‘𝐴) = ((vol* ↾ dom vol)‘𝐴)
3		fvres 6900	. 2 ⊢ (𝐴 ∈ dom vol → ((vol* ↾ dom vol)‘𝐴) = (vol*‘𝐴))
4	2, 3	eqtrid 2810	1 ⊢ (𝐴 ∈ dom vol → (vol‘𝐴) = (vol*‘𝐴))

Syntax hints:   → wi 4   = wceq 1570   ∈ wcel 2143  dom cdm 5661   ↾ cres 5663  ‘cfv 6536  vol*covol 25621  volcvol 25622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5257  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-xp 5667  df-rel 5668  df-cnv 5669  df-dm 5671  df-rn 5672  df-res 5673  df-iota 6492  df-fv 6544  df-vol 25624

This theorem is referenced by:  volss  25692  volun  25704  volinun  25705  volfiniun  25706  voliunlem3  25711  volsup  25715  iccvolcl  25726  ovolioo  25727  volioo  25728  ioovolcl  25729  uniioovol  25738  uniioombllem4  25745  volcn  25765  volivth  25766  vitalilem4  25770  i1fima2  25838  i1fd  25840  i1f0rn  25841  itg1val2  25843  itg1ge0  25845  itg11  25850  i1fadd  25854  i1fmul  25855  itg1addlem2  25856  itg1addlem4  25858  i1fres  25864  itg10a  25869  itg1ge0a  25870  itg1climres  25873  mbfi1fseqlem4  25877  itg2const2  25900  itg2gt0  25919  itg2cnlem2  25921  ftc1a  26196  ftc1lem4  26198  itgulm  26571  areaf  27126  cntnevol  34618  volmeas  34621  mblfinlem3  38330  mblfinlem4  38331  ismblfin  38332  voliunnfl  38335  volsupnfl  38336  itg2addnclem  38342  itg2addnclem2  38343  itg2gt0cn  38346  ftc1cnnclem  38362  ftc1anclem7  38370  areacirc  38384  arearect  43962  areaquad  43963  vol0  46693  volge0  46695  volsn  46701  volicc  46732  vonvol  47396