Theorem mblvol 25761

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 25759	. . 3 ⊢ vol = (vol* ↾ dom vol)
2	1	fveq1i 6880	. 2 ⊢ (vol‘𝐴) = ((vol* ↾ dom vol)‘𝐴)
3		fvres 6898	. 2 ⊢ (𝐴 ∈ dom vol → ((vol* ↾ dom vol)‘𝐴) = (vol*‘𝐴))
4	2, 3	eqtrid 2807	1 ⊢ (𝐴 ∈ dom vol → (vol‘𝐴) = (vol*‘𝐴))

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  dom cdm 5655   ↾ cres 5657  ‘cfv 6533  vol*covol 25693  volcvol 25694

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 2732  ax-sep 5251  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 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  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 5661  df-rel 5662  df-cnv 5663  df-dm 5665  df-rn 5666  df-res 5667  df-iota 6489  df-fv 6541  df-vol 25696

This theorem is used by:  volss  25764  volun  25776  volinun  25777  volfiniun  25778  voliunlem3  25783  volsup  25787  iccvolcl  25798  ovolioo  25799  volioo  25800  ioovolcl  25801  uniioovol  25810  uniioombllem4  25817  volcn  25837  volivth  25838  vitalilem4  25842  i1fima2  25910  i1fd  25912  i1f0rn  25913  itg1val2  25915  itg1ge0  25917  itg11  25922  i1fadd  25926  i1fmul  25927  itg1addlem2  25928  itg1addlem4  25930  i1fres  25936  itg10a  25941  itg1ge0a  25942  itg1climres  25945  mbfi1fseqlem4  25949  itg2const2  25972  itg2gt0  25991  itg2cnlem2  25993  ftc1a  26267  ftc1lem4  26269  itgulm  26647  areaf  27201  cntnevol  34742  volmeas  34745  mblfinlem3  38411  mblfinlem4  38412  ismblfin  38413  voliunnfl  38416  volsupnfl  38417  itg2addnclem  38423  itg2addnclem2  38424  itg2gt0cn  38427  ftc1cnnclem  38443  ftc1anclem7  38451  areacirc  38465  arearect  44059  areaquad  44060  vol0  46790  volge0  46792  volsn  46798  volicc  46829  vonvol  47493