Detailed syntax breakdown of Definition df-cxp
Step | Hyp | Ref
| Expression |
1 | | ccxp 24302 |
. 2
class
↑𝑐 |
2 | | vx |
. . 3
setvar 𝑥 |
3 | | vy |
. . 3
setvar 𝑦 |
4 | | cc 9934 |
. . 3
class
ℂ |
5 | 2 | cv 1482 |
. . . . 5
class 𝑥 |
6 | | cc0 9936 |
. . . . 5
class
0 |
7 | 5, 6 | wceq 1483 |
. . . 4
wff 𝑥 = 0 |
8 | 3 | cv 1482 |
. . . . . 6
class 𝑦 |
9 | 8, 6 | wceq 1483 |
. . . . 5
wff 𝑦 = 0 |
10 | | c1 9937 |
. . . . 5
class
1 |
11 | 9, 10, 6 | cif 4086 |
. . . 4
class if(𝑦 = 0, 1, 0) |
12 | | clog 24301 |
. . . . . . 7
class
log |
13 | 5, 12 | cfv 5888 |
. . . . . 6
class
(log‘𝑥) |
14 | | cmul 9941 |
. . . . . 6
class
· |
15 | 8, 13, 14 | co 6650 |
. . . . 5
class (𝑦 · (log‘𝑥)) |
16 | | ce 14792 |
. . . . 5
class
exp |
17 | 15, 16 | cfv 5888 |
. . . 4
class
(exp‘(𝑦
· (log‘𝑥))) |
18 | 7, 11, 17 | cif 4086 |
. . 3
class if(𝑥 = 0, if(𝑦 = 0, 1, 0), (exp‘(𝑦 · (log‘𝑥)))) |
19 | 2, 3, 4, 4, 18 | cmpt2 6652 |
. 2
class (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ if(𝑥 = 0, if(𝑦 = 0, 1, 0), (exp‘(𝑦 · (log‘𝑥))))) |
20 | 1, 19 | wceq 1483 |
1
wff
↑𝑐 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ if(𝑥 = 0, if(𝑦 = 0, 1, 0), (exp‘(𝑦 · (log‘𝑥))))) |