Detailed syntax breakdown of Definition df-evpm
Step | Hyp | Ref
| Expression |
1 | | cevpm 18391 |
. 2
class
pmEven |
2 | | vd |
. . 3
setvar 𝑑 |
3 | | cvv 3408 |
. . 3
class
V |
4 | 2 | cv 1507 |
. . . . . 6
class 𝑑 |
5 | | cpsgn 18390 |
. . . . . 6
class
pmSgn |
6 | 4, 5 | cfv 6185 |
. . . . 5
class
(pmSgn‘𝑑) |
7 | 6 | ccnv 5402 |
. . . 4
class ◡(pmSgn‘𝑑) |
8 | | c1 10334 |
. . . . 5
class
1 |
9 | 8 | csn 4435 |
. . . 4
class
{1} |
10 | 7, 9 | cima 5406 |
. . 3
class (◡(pmSgn‘𝑑) “ {1}) |
11 | 2, 3, 10 | cmpt 5004 |
. 2
class (𝑑 ∈ V ↦ (◡(pmSgn‘𝑑) “ {1})) |
12 | 1, 11 | wceq 1508 |
1
wff pmEven =
(𝑑 ∈ V ↦ (◡(pmSgn‘𝑑) “ {1})) |