Detailed syntax breakdown of Definition df-oadd
| Step | Hyp | Ref
| Expression |
| 1 | | coa 8503 |
. 2
class
+o |
| 2 | | vx |
. . 3
setvar 𝑥 |
| 3 | | vy |
. . 3
setvar 𝑦 |
| 4 | | con0 6384 |
. . 3
class
On |
| 5 | 3 | cv 1539 |
. . . 4
class 𝑦 |
| 6 | | vz |
. . . . . 6
setvar 𝑧 |
| 7 | | cvv 3480 |
. . . . . 6
class
V |
| 8 | 6 | cv 1539 |
. . . . . . 7
class 𝑧 |
| 9 | 8 | csuc 6386 |
. . . . . 6
class suc 𝑧 |
| 10 | 6, 7, 9 | cmpt 5225 |
. . . . 5
class (𝑧 ∈ V ↦ suc 𝑧) |
| 11 | 2 | cv 1539 |
. . . . 5
class 𝑥 |
| 12 | 10, 11 | crdg 8449 |
. . . 4
class
rec((𝑧 ∈ V
↦ suc 𝑧), 𝑥) |
| 13 | 5, 12 | cfv 6561 |
. . 3
class
(rec((𝑧 ∈ V
↦ suc 𝑧), 𝑥)‘𝑦) |
| 14 | 2, 3, 4, 4, 13 | cmpo 7433 |
. 2
class (𝑥 ∈ On, 𝑦 ∈ On ↦ (rec((𝑧 ∈ V ↦ suc 𝑧), 𝑥)‘𝑦)) |
| 15 | 1, 14 | wceq 1540 |
1
wff
+o = (𝑥 ∈
On, 𝑦 ∈ On ↦
(rec((𝑧 ∈ V ↦
suc 𝑧), 𝑥)‘𝑦)) |