Detailed syntax breakdown of Definition df-negs
Step | Hyp | Ref
| Expression |
1 | | cnegs 34044 |
. 2
class
-us |
2 | | vx |
. . . 4
setvar 𝑥 |
3 | | vn |
. . . 4
setvar 𝑛 |
4 | | cvv 3422 |
. . . 4
class
V |
5 | 3 | cv 1538 |
. . . . . 6
class 𝑛 |
6 | 2 | cv 1538 |
. . . . . . 7
class 𝑥 |
7 | | cright 33957 |
. . . . . . 7
class
R |
8 | 6, 7 | cfv 6418 |
. . . . . 6
class ( R
‘𝑥) |
9 | 5, 8 | cima 5583 |
. . . . 5
class (𝑛 “ ( R ‘𝑥)) |
10 | | cleft 33956 |
. . . . . . 7
class
L |
11 | 6, 10 | cfv 6418 |
. . . . . 6
class ( L
‘𝑥) |
12 | 5, 11 | cima 5583 |
. . . . 5
class (𝑛 “ ( L ‘𝑥)) |
13 | | cscut 33904 |
. . . . 5
class
|s |
14 | 9, 12, 13 | co 7255 |
. . . 4
class ((𝑛 “ ( R ‘𝑥)) |s (𝑛 “ ( L ‘𝑥))) |
15 | 2, 3, 4, 4, 14 | cmpo 7257 |
. . 3
class (𝑥 ∈ V, 𝑛 ∈ V ↦ ((𝑛 “ ( R ‘𝑥)) |s (𝑛 “ ( L ‘𝑥)))) |
16 | 15 | cnorec 34021 |
. 2
class norec
((𝑥 ∈ V, 𝑛 ∈ V ↦ ((𝑛 “ ( R ‘𝑥)) |s (𝑛 “ ( L ‘𝑥))))) |
17 | 1, 16 | wceq 1539 |
1
wff -us =
norec ((𝑥 ∈ V, 𝑛 ∈ V ↦ ((𝑛 “ ( R ‘𝑥)) |s (𝑛 “ ( L ‘𝑥))))) |