# Metamath Proof Explorer

## Definition df-vol

Description: Define the Lebesgue measure, which is just the outer measure with a peculiar domain of definition. The property of being Lebesgue-measurable can be expressed as A e. dom vol . (Contributed by Mario Carneiro, 17-Mar-2014)

Ref Expression
Assertion df-vol $⊢ vol = vol * ↾ x | ∀ y ∈ vol * -1 ℝ vol * ⁡ y = vol * ⁡ y ∩ x + vol * ⁡ y ∖ x$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cvol $class vol$
1 covol $class vol *$
2 vx $setvar x$
3 vy $setvar y$
4 1 ccnv $class vol * -1$
5 cr $class ℝ$
6 4 5 cima $class vol * -1 ℝ$
7 3 cv $setvar y$
8 7 1 cfv $class vol * ⁡ y$
9 2 cv $setvar x$
10 7 9 cin $class y ∩ x$
11 10 1 cfv $class vol * ⁡ y ∩ x$
12 caddc $class +$
13 7 9 cdif $class y ∖ x$
14 13 1 cfv $class vol * ⁡ y ∖ x$
15 11 14 12 co $class vol * ⁡ y ∩ x + vol * ⁡ y ∖ x$
16 8 15 wceq $wff vol * ⁡ y = vol * ⁡ y ∩ x + vol * ⁡ y ∖ x$
17 16 3 6 wral $wff ∀ y ∈ vol * -1 ℝ vol * ⁡ y = vol * ⁡ y ∩ x + vol * ⁡ y ∖ x$
18 17 2 cab $class x | ∀ y ∈ vol * -1 ℝ vol * ⁡ y = vol * ⁡ y ∩ x + vol * ⁡ y ∖ x$
19 1 18 cres $class vol * ↾ x | ∀ y ∈ vol * -1 ℝ vol * ⁡ y = vol * ⁡ y ∩ x + vol * ⁡ y ∖ x$
20 0 19 wceq $wff vol = vol * ↾ x | ∀ y ∈ vol * -1 ℝ vol * ⁡ y = vol * ⁡ y ∩ x + vol * ⁡ y ∖ x$