Theorem mblvol 25502

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 25500	. . 3 ⊢ vol = (vol* ↾ dom vol)
2	1	fveq1i 6843	. 2 ⊢ (vol‘𝐴) = ((vol* ↾ dom vol)‘𝐴)
3		fvres 6861	. 2 ⊢ (𝐴 ∈ dom vol → ((vol* ↾ dom vol)‘𝐴) = (vol*‘𝐴))
4	2, 3	eqtrid 2784	1 ⊢ (𝐴 ∈ dom vol → (vol‘𝐴) = (vol*‘𝐴))

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  dom cdm 5632   ↾ cres 5634  ‘cfv 6500  vol*covol 25434  volcvol 25435

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5243  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-xp 5638  df-rel 5639  df-cnv 5640  df-dm 5642  df-rn 5643  df-res 5644  df-iota 6456  df-fv 6508  df-vol 25437

This theorem is referenced by:  volss  25505  volun  25517  volinun  25518  volfiniun  25519  voliunlem3  25524  volsup  25528  iccvolcl  25539  ovolioo  25540  volioo  25541  ioovolcl  25542  uniioovol  25551  uniioombllem4  25558  volcn  25578  volivth  25579  vitalilem4  25583  i1fima2  25651  i1fd  25653  i1f0rn  25654  itg1val2  25656  itg1ge0  25658  itg11  25663  i1fadd  25667  i1fmul  25668  itg1addlem2  25669  itg1addlem4  25671  i1fres  25677  itg10a  25682  itg1ge0a  25683  itg1climres  25686  mbfi1fseqlem4  25690  itg2const2  25713  itg2gt0  25732  itg2cnlem2  25734  ftc1a  26015  ftc1lem4  26017  itgulm  26388  areaf  26942  cntnevol  34410  volmeas  34413  mblfinlem3  37914  mblfinlem4  37915  ismblfin  37916  voliunnfl  37919  volsupnfl  37920  itg2addnclem  37926  itg2addnclem2  37927  itg2gt0cn  37930  ftc1cnnclem  37946  ftc1anclem7  37954  areacirc  37968  arearect  43576  areaquad  43577  vol0  46321  volge0  46323  volsn  46329  volicc  46360  vonvol  47024