Detailed syntax breakdown of Definition df-vol
Step | Hyp | Ref
| Expression |
1 | | cvol 24636 |
. 2
class
vol |
2 | | covol 24635 |
. . 3
class
vol* |
3 | | vy |
. . . . . . . 8
setvar 𝑦 |
4 | 3 | cv 1538 |
. . . . . . 7
class 𝑦 |
5 | 4, 2 | cfv 6437 |
. . . . . 6
class
(vol*‘𝑦) |
6 | | vx |
. . . . . . . . . 10
setvar 𝑥 |
7 | 6 | cv 1538 |
. . . . . . . . 9
class 𝑥 |
8 | 4, 7 | cin 3887 |
. . . . . . . 8
class (𝑦 ∩ 𝑥) |
9 | 8, 2 | cfv 6437 |
. . . . . . 7
class
(vol*‘(𝑦 ∩
𝑥)) |
10 | 4, 7 | cdif 3885 |
. . . . . . . 8
class (𝑦 ∖ 𝑥) |
11 | 10, 2 | cfv 6437 |
. . . . . . 7
class
(vol*‘(𝑦
∖ 𝑥)) |
12 | | caddc 10883 |
. . . . . . 7
class
+ |
13 | 9, 11, 12 | co 7284 |
. . . . . 6
class
((vol*‘(𝑦
∩ 𝑥)) +
(vol*‘(𝑦 ∖
𝑥))) |
14 | 5, 13 | wceq 1539 |
. . . . 5
wff
(vol*‘𝑦) =
((vol*‘(𝑦 ∩ 𝑥)) + (vol*‘(𝑦 ∖ 𝑥))) |
15 | 2 | ccnv 5589 |
. . . . . 6
class ◡vol* |
16 | | cr 10879 |
. . . . . 6
class
ℝ |
17 | 15, 16 | cima 5593 |
. . . . 5
class (◡vol* “ ℝ) |
18 | 14, 3, 17 | wral 3065 |
. . . 4
wff
∀𝑦 ∈
(◡vol* “
ℝ)(vol*‘𝑦) =
((vol*‘(𝑦 ∩ 𝑥)) + (vol*‘(𝑦 ∖ 𝑥))) |
19 | 18, 6 | cab 2716 |
. . 3
class {𝑥 ∣ ∀𝑦 ∈ (◡vol* “ ℝ)(vol*‘𝑦) = ((vol*‘(𝑦 ∩ 𝑥)) + (vol*‘(𝑦 ∖ 𝑥)))} |
20 | 2, 19 | cres 5592 |
. 2
class (vol*
↾ {𝑥 ∣
∀𝑦 ∈ (◡vol* “ ℝ)(vol*‘𝑦) = ((vol*‘(𝑦 ∩ 𝑥)) + (vol*‘(𝑦 ∖ 𝑥)))}) |
21 | 1, 20 | wceq 1539 |
1
wff vol = (vol*
↾ {𝑥 ∣
∀𝑦 ∈ (◡vol* “ ℝ)(vol*‘𝑦) = ((vol*‘(𝑦 ∩ 𝑥)) + (vol*‘(𝑦 ∖ 𝑥)))}) |