Detailed syntax breakdown of Definition df-norec
Step | Hyp | Ref
| Expression |
1 | | cF |
. . 3
class 𝐹 |
2 | 1 | cnorec 33857 |
. 2
class norec
(𝐹) |
3 | | csur 33606 |
. . 3
class No |
4 | | vx |
. . . . . 6
setvar 𝑥 |
5 | 4 | cv 1542 |
. . . . 5
class 𝑥 |
6 | | vy |
. . . . . . . 8
setvar 𝑦 |
7 | 6 | cv 1542 |
. . . . . . 7
class 𝑦 |
8 | | cleft 33792 |
. . . . . . 7
class
L |
9 | 7, 8 | cfv 6398 |
. . . . . 6
class ( L
‘𝑦) |
10 | | cright 33793 |
. . . . . . 7
class
R |
11 | 7, 10 | cfv 6398 |
. . . . . 6
class ( R
‘𝑦) |
12 | 9, 11 | cun 3879 |
. . . . 5
class (( L
‘𝑦) ∪ ( R
‘𝑦)) |
13 | 5, 12 | wcel 2111 |
. . . 4
wff 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦)) |
14 | 13, 4, 6 | copab 5130 |
. . 3
class
{〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))} |
15 | 3, 14, 1 | cfrecs 8043 |
. 2
class
frecs({〈𝑥,
𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))}, No
, 𝐹) |
16 | 2, 15 | wceq 1543 |
1
wff norec
(𝐹) = frecs({〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))}, No , 𝐹) |