Detailed syntax breakdown of Definition df-cj
Step | Hyp | Ref
| Expression |
1 | | ccj 14816 |
. 2
class
∗ |
2 | | vx |
. . 3
setvar 𝑥 |
3 | | cc 10878 |
. . 3
class
ℂ |
4 | 2 | cv 1538 |
. . . . . . 7
class 𝑥 |
5 | | vy |
. . . . . . . 8
setvar 𝑦 |
6 | 5 | cv 1538 |
. . . . . . 7
class 𝑦 |
7 | | caddc 10883 |
. . . . . . 7
class
+ |
8 | 4, 6, 7 | co 7284 |
. . . . . 6
class (𝑥 + 𝑦) |
9 | | cr 10879 |
. . . . . 6
class
ℝ |
10 | 8, 9 | wcel 2107 |
. . . . 5
wff (𝑥 + 𝑦) ∈ ℝ |
11 | | ci 10882 |
. . . . . . 7
class
i |
12 | | cmin 11214 |
. . . . . . . 8
class
− |
13 | 4, 6, 12 | co 7284 |
. . . . . . 7
class (𝑥 − 𝑦) |
14 | | cmul 10885 |
. . . . . . 7
class
· |
15 | 11, 13, 14 | co 7284 |
. . . . . 6
class (i
· (𝑥 − 𝑦)) |
16 | 15, 9 | wcel 2107 |
. . . . 5
wff (i ·
(𝑥 − 𝑦)) ∈
ℝ |
17 | 10, 16 | wa 396 |
. . . 4
wff ((𝑥 + 𝑦) ∈ ℝ ∧ (i · (𝑥 − 𝑦)) ∈ ℝ) |
18 | 17, 5, 3 | crio 7240 |
. . 3
class
(℩𝑦
∈ ℂ ((𝑥 + 𝑦) ∈ ℝ ∧ (i
· (𝑥 − 𝑦)) ∈
ℝ)) |
19 | 2, 3, 18 | cmpt 5158 |
. 2
class (𝑥 ∈ ℂ ↦
(℩𝑦 ∈
ℂ ((𝑥 + 𝑦) ∈ ℝ ∧ (i
· (𝑥 − 𝑦)) ∈
ℝ))) |
20 | 1, 19 | wceq 1539 |
1
wff ∗ =
(𝑥 ∈ ℂ ↦
(℩𝑦 ∈
ℂ ((𝑥 + 𝑦) ∈ ℝ ∧ (i
· (𝑥 − 𝑦)) ∈
ℝ))) |