Step | Hyp | Ref
| Expression |
1 | | cnegs 27321 |
. 2
class
-us |
2 | | vx |
. . . 4
setvar 𝑥 |
3 | | vn |
. . . 4
setvar 𝑛 |
4 | | cvv 3446 |
. . . 4
class
V |
5 | 3 | cv 1541 |
. . . . . 6
class 𝑛 |
6 | 2 | cv 1541 |
. . . . . . 7
class 𝑥 |
7 | | cright 27179 |
. . . . . . 7
class
R |
8 | 6, 7 | cfv 6497 |
. . . . . 6
class ( R
‘𝑥) |
9 | 5, 8 | cima 5637 |
. . . . 5
class (𝑛 “ ( R ‘𝑥)) |
10 | | cleft 27178 |
. . . . . . 7
class
L |
11 | 6, 10 | cfv 6497 |
. . . . . 6
class ( L
‘𝑥) |
12 | 5, 11 | cima 5637 |
. . . . 5
class (𝑛 “ ( L ‘𝑥)) |
13 | | cscut 27125 |
. . . . 5
class
|s |
14 | 9, 12, 13 | co 7358 |
. . . 4
class ((𝑛 “ ( R ‘𝑥)) |s (𝑛 “ ( L ‘𝑥))) |
15 | 2, 3, 4, 4, 14 | cmpo 7360 |
. . 3
class (𝑥 ∈ V, 𝑛 ∈ V ↦ ((𝑛 “ ( R ‘𝑥)) |s (𝑛 “ ( L ‘𝑥)))) |
16 | 15 | cnorec 27252 |
. 2
class norec
((𝑥 ∈ V, 𝑛 ∈ V ↦ ((𝑛 “ ( R ‘𝑥)) |s (𝑛 “ ( L ‘𝑥))))) |
17 | 1, 16 | wceq 1542 |
1
wff
-us = norec ((𝑥
∈ V, 𝑛 ∈ V
↦ ((𝑛 “ ( R
‘𝑥)) |s (𝑛 “ ( L ‘𝑥))))) |