Detailed syntax breakdown of Definition df-evpm
Step | Hyp | Ref
| Expression |
1 | | cevpm 17910 |
. 2
class
pmEven |
2 | | vd |
. . 3
setvar 𝑑 |
3 | | cvv 3200 |
. . 3
class
V |
4 | 2 | cv 1482 |
. . . . . 6
class 𝑑 |
5 | | cpsgn 17909 |
. . . . . 6
class
pmSgn |
6 | 4, 5 | cfv 5888 |
. . . . 5
class
(pmSgn‘𝑑) |
7 | 6 | ccnv 5113 |
. . . 4
class ◡(pmSgn‘𝑑) |
8 | | c1 9937 |
. . . . 5
class
1 |
9 | 8 | csn 4177 |
. . . 4
class
{1} |
10 | 7, 9 | cima 5117 |
. . 3
class (◡(pmSgn‘𝑑) “ {1}) |
11 | 2, 3, 10 | cmpt 4729 |
. 2
class (𝑑 ∈ V ↦ (◡(pmSgn‘𝑑) “ {1})) |
12 | 1, 11 | wceq 1483 |
1
wff pmEven =
(𝑑 ∈ V ↦ (◡(pmSgn‘𝑑) “ {1})) |