Theorem mblvol

Description: The volume of a measurable set is the same as its outer volume. (Contributed by Mario Carneiro, 17-Mar-2014)

	Ref	Expression
Assertion	mblvol	$$⊢A\in \mathrm{dom}vol\to vol\left(A\right)={vol}^{*}\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		volres	$$⊢vol={{vol}^{*}\upharpoonright }_{\mathrm{dom}vol}$$
2	1	fveq1i	$$⊢vol\left(A\right)=\left({{vol}^{*}\upharpoonright }_{\mathrm{dom}vol}\right)\left(A\right)$$
3		fvres	$$⊢A\in \mathrm{dom}vol\to \left({{vol}^{*}\upharpoonright }_{\mathrm{dom}vol}\right)\left(A\right)={vol}^{*}\left(A\right)$$
4	2 3	syl5eq	$$⊢A\in \mathrm{dom}vol\to vol\left(A\right)={vol}^{*}\left(A\right)$$