Theorem mblvol 25906

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2147  dom cdm 5658   ↾ cres 5660  ‘cfv 6566  vol*covol 25838  volcvol 25839

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5255  ax-pr 5398

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-opab 5174  df-xp 5664  df-rel 5665  df-cnv 5666  df-dm 5668  df-rn 5669  df-res 5670  df-iota 6520  df-fv 6574  df-vol 25841

This theorem is used by:  volss  25909  volun  25921  volinun  25922  volfiniun  25923  voliunlem3  25928  volsup  25932  iccvolcl  25943  ovolioo  25944  volioo  25945  ioovolcl  25946  uniioovol  25955  uniioombllem4  25962  volcn  25982  volivth  25983  vitalilem4  25987  i1fima2  26055  i1fd  26057  i1f0rn  26058  itg1val2  26060  itg1ge0  26062  itg11  26067  i1fadd  26071  i1fmul  26072  itg1addlem2  26073  itg1addlem4  26075  i1fres  26081  itg10a  26086  itg1ge0a  26087  itg1climres  26090  mbfi1fseqlem4  26094  itg2const2  26117  itg2gt0  26136  itg2cnlem2  26138  ftc1a  26412  ftc1lem4  26414  itgulm  26792  areaf  27346  cntnevol  34972  volmeas  34975  mblfinlem3  38845  mblfinlem4  38846  ismblfin  38847  voliunnfl  38850  volsupnfl  38851  itg2addnclem  38857  itg2addnclem2  38858  itg2gt0cn  38861  ftc1cnnclem  38877  ftc1anclem7  38885  areacirc  38899  arearect  44478  areaquad  44479  vol0  47242  volge0  47244  volsn  47250  volicc  47281  vonvol  47945