Detailed syntax breakdown of Definition df-gbo
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | cgbo 47734 | . 2
class 
GoldbachOdd | 
| 2 |  | vp | . . . . . . . . . 10
setvar 𝑝 | 
| 3 | 2 | cv 1539 | . . . . . . . . 9
class 𝑝 | 
| 4 |  | codd 47612 | . . . . . . . . 9
class 
Odd | 
| 5 | 3, 4 | wcel 2108 | . . . . . . . 8
wff 𝑝 ∈ Odd | 
| 6 |  | vq | . . . . . . . . . 10
setvar 𝑞 | 
| 7 | 6 | cv 1539 | . . . . . . . . 9
class 𝑞 | 
| 8 | 7, 4 | wcel 2108 | . . . . . . . 8
wff 𝑞 ∈ Odd | 
| 9 |  | vr | . . . . . . . . . 10
setvar 𝑟 | 
| 10 | 9 | cv 1539 | . . . . . . . . 9
class 𝑟 | 
| 11 | 10, 4 | wcel 2108 | . . . . . . . 8
wff 𝑟 ∈ Odd | 
| 12 | 5, 8, 11 | w3a 1087 | . . . . . . 7
wff (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) | 
| 13 |  | vz | . . . . . . . . 9
setvar 𝑧 | 
| 14 | 13 | cv 1539 | . . . . . . . 8
class 𝑧 | 
| 15 |  | caddc 11158 | . . . . . . . . . 10
class 
+ | 
| 16 | 3, 7, 15 | co 7431 | . . . . . . . . 9
class (𝑝 + 𝑞) | 
| 17 | 16, 10, 15 | co 7431 | . . . . . . . 8
class ((𝑝 + 𝑞) + 𝑟) | 
| 18 | 14, 17 | wceq 1540 | . . . . . . 7
wff 𝑧 = ((𝑝 + 𝑞) + 𝑟) | 
| 19 | 12, 18 | wa 395 | . . . . . 6
wff ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑧 = ((𝑝 + 𝑞) + 𝑟)) | 
| 20 |  | cprime 16708 | . . . . . 6
class
ℙ | 
| 21 | 19, 9, 20 | wrex 3070 | . . . . 5
wff
∃𝑟 ∈
ℙ ((𝑝 ∈ Odd
∧ 𝑞 ∈ Odd ∧
𝑟 ∈ Odd ) ∧ 𝑧 = ((𝑝 + 𝑞) + 𝑟)) | 
| 22 | 21, 6, 20 | wrex 3070 | . . . 4
wff
∃𝑞 ∈
ℙ ∃𝑟 ∈
ℙ ((𝑝 ∈ Odd
∧ 𝑞 ∈ Odd ∧
𝑟 ∈ Odd ) ∧ 𝑧 = ((𝑝 + 𝑞) + 𝑟)) | 
| 23 | 22, 2, 20 | wrex 3070 | . . 3
wff
∃𝑝 ∈
ℙ ∃𝑞 ∈
ℙ ∃𝑟 ∈
ℙ ((𝑝 ∈ Odd
∧ 𝑞 ∈ Odd ∧
𝑟 ∈ Odd ) ∧ 𝑧 = ((𝑝 + 𝑞) + 𝑟)) | 
| 24 | 23, 13, 4 | crab 3436 | . 2
class {𝑧 ∈ Odd ∣ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑧 = ((𝑝 + 𝑞) + 𝑟))} | 
| 25 | 1, 24 | wceq 1540 | 1
wff 
GoldbachOdd = {𝑧 ∈ Odd
∣ ∃𝑝 ∈
ℙ ∃𝑞 ∈
ℙ ∃𝑟 ∈
ℙ ((𝑝 ∈ Odd
∧ 𝑞 ∈ Odd ∧
𝑟 ∈ Odd ) ∧ 𝑧 = ((𝑝 + 𝑞) + 𝑟))} |