Theorem mblvol 25863

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 25861	. . 3 ⊢ vol = (vol* ↾ dom vol)
2	1	fveq1i 6894	. 2 ⊢ (vol‘𝐴) = ((vol* ↾ dom vol)‘𝐴)
3		fvres 6912	. 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 1569   ∈ wcel 2146  dom cdm 5654   ↾ cres 5656  ‘cfv 6546  vol*covol 25795  volcvol 25796

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735  ax-sep 5251  ax-pr 5394

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-rab 3416  df-v 3455  df-ss 3900  df-dif 4049  df-in 4093  df-un 4153  df-nul 4281  df-if 4485  df-sn 4588  df-pr 4590  df-op 4838  df-uni 4870  df-br 5106  df-opab 5170  df-xp 5660  df-rel 5661  df-cnv 5662  df-dm 5664  df-rn 5665  df-res 5666  df-iota 6500  df-fv 6554  df-vol 25798

This theorem is used by:  volss  25866  volun  25878  volinun  25879  volfiniun  25880  voliunlem3  25885  volsup  25889  iccvolcl  25900  ovolioo  25901  volioo  25902  ioovolcl  25903  uniioovol  25912  uniioombllem4  25919  volcn  25939  volivth  25940  vitalilem4  25944  i1fima2  26012  i1fd  26014  i1f0rn  26015  itg1val2  26017  itg1ge0  26019  itg11  26024  i1fadd  26028  i1fmul  26029  itg1addlem2  26030  itg1addlem4  26032  i1fres  26038  itg10a  26043  itg1ge0a  26044  itg1climres  26047  mbfi1fseqlem4  26051  itg2const2  26074  itg2gt0  26093  itg2cnlem2  26095  ftc1a  26369  ftc1lem4  26371  itgulm  26747  areaf  27301  cntnevol  34914  volmeas  34917  mblfinlem3  38717  mblfinlem4  38718  ismblfin  38719  voliunnfl  38722  volsupnfl  38723  itg2addnclem  38729  itg2addnclem2  38730  itg2gt0cn  38733  ftc1cnnclem  38749  ftc1anclem7  38757  areacirc  38771  arearect  44357  areaquad  44358  vol0  47108  volge0  47110  volsn  47116  volicc  47147  vonvol  47811