Theorem mblvol 23498

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 23496	. . 3 ⊢ vol = (vol* ↾ dom vol)
2	1	fveq1i 6353	. 2 ⊢ (vol‘𝐴) = ((vol* ↾ dom vol)‘𝐴)
3		fvres 6368	. 2 ⊢ (𝐴 ∈ dom vol → ((vol* ↾ dom vol)‘𝐴) = (vol*‘𝐴))
4	2, 3	syl5eq 2806	1 ⊢ (𝐴 ∈ dom vol → (vol‘𝐴) = (vol*‘𝐴))

Syntax hints:   → wi 4   = wceq 1632   ∈ wcel 2139  dom cdm 5266   ↾ cres 5268  ‘cfv 6049  vol*covol 23431  volcvol 23432

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pr 5055

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ral 3055  df-rex 3056  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-br 4805  df-opab 4865  df-xp 5272  df-rel 5273  df-cnv 5274  df-dm 5276  df-rn 5277  df-res 5278  df-iota 6012  df-fv 6057  df-vol 23434

This theorem is referenced by:  volss  23501  volun  23513  volinun  23514  volfiniun  23515  voliunlem3  23520  volsup  23524  iccvolcl  23535  ovolioo  23536  volioo  23537  ioovolcl  23538  uniioovol  23547  uniioombllem4  23554  volcn  23574  volivth  23575  vitalilem4  23579  i1fima2  23645  i1fd  23647  i1f0rn  23648  itg1val2  23650  itg1ge0  23652  itg11  23657  i1fadd  23661  i1fmul  23662  itg1addlem2  23663  itg1addlem4  23665  i1fres  23671  itg10a  23676  itg1ge0a  23677  itg1climres  23680  mbfi1fseqlem4  23684  itg2const2  23707  itg2gt0  23726  itg2cnlem2  23728  ftc1a  23999  ftc1lem4  24001  itgulm  24361  areaf  24887  cntnevol  30600  volmeas  30603  mblfinlem3  33761  mblfinlem4  33762  ismblfin  33763  voliunnfl  33766  volsupnfl  33767  itg2addnclem  33774  itg2addnclem2  33775  itg2gt0cn  33778  ftc1cnnclem  33796  ftc1anclem7  33804  areacirc  33818  arearect  38303  areaquad  38304  vol0  40678  volge0  40680  volsn  40686  volicc  40718  vonvol  41382