Detailed syntax breakdown of Definition df-gbo
Step | Hyp | Ref
| Expression |
1 | | cgbo 44905 |
. 2
class
GoldbachOdd |
2 | | vp |
. . . . . . . . . 10
setvar 𝑝 |
3 | 2 | cv 1542 |
. . . . . . . . 9
class 𝑝 |
4 | | codd 44783 |
. . . . . . . . 9
class
Odd |
5 | 3, 4 | wcel 2112 |
. . . . . . . 8
wff 𝑝 ∈ Odd |
6 | | vq |
. . . . . . . . . 10
setvar 𝑞 |
7 | 6 | cv 1542 |
. . . . . . . . 9
class 𝑞 |
8 | 7, 4 | wcel 2112 |
. . . . . . . 8
wff 𝑞 ∈ Odd |
9 | | vr |
. . . . . . . . . 10
setvar 𝑟 |
10 | 9 | cv 1542 |
. . . . . . . . 9
class 𝑟 |
11 | 10, 4 | wcel 2112 |
. . . . . . . 8
wff 𝑟 ∈ Odd |
12 | 5, 8, 11 | w3a 1089 |
. . . . . . 7
wff (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) |
13 | | vz |
. . . . . . . . 9
setvar 𝑧 |
14 | 13 | cv 1542 |
. . . . . . . 8
class 𝑧 |
15 | | caddc 10759 |
. . . . . . . . . 10
class
+ |
16 | 3, 7, 15 | co 7234 |
. . . . . . . . 9
class (𝑝 + 𝑞) |
17 | 16, 10, 15 | co 7234 |
. . . . . . . 8
class ((𝑝 + 𝑞) + 𝑟) |
18 | 14, 17 | wceq 1543 |
. . . . . . 7
wff 𝑧 = ((𝑝 + 𝑞) + 𝑟) |
19 | 12, 18 | wa 399 |
. . . . . 6
wff ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑧 = ((𝑝 + 𝑞) + 𝑟)) |
20 | | cprime 16258 |
. . . . . 6
class
ℙ |
21 | 19, 9, 20 | wrex 3064 |
. . . . 5
wff
∃𝑟 ∈
ℙ ((𝑝 ∈ Odd
∧ 𝑞 ∈ Odd ∧
𝑟 ∈ Odd ) ∧ 𝑧 = ((𝑝 + 𝑞) + 𝑟)) |
22 | 21, 6, 20 | wrex 3064 |
. . . 4
wff
∃𝑞 ∈
ℙ ∃𝑟 ∈
ℙ ((𝑝 ∈ Odd
∧ 𝑞 ∈ Odd ∧
𝑟 ∈ Odd ) ∧ 𝑧 = ((𝑝 + 𝑞) + 𝑟)) |
23 | 22, 2, 20 | wrex 3064 |
. . 3
wff
∃𝑝 ∈
ℙ ∃𝑞 ∈
ℙ ∃𝑟 ∈
ℙ ((𝑝 ∈ Odd
∧ 𝑞 ∈ Odd ∧
𝑟 ∈ Odd ) ∧ 𝑧 = ((𝑝 + 𝑞) + 𝑟)) |
24 | 23, 13, 4 | crab 3067 |
. 2
class {𝑧 ∈ Odd ∣ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑧 = ((𝑝 + 𝑞) + 𝑟))} |
25 | 1, 24 | wceq 1543 |
1
wff
GoldbachOdd = {𝑧 ∈ Odd
∣ ∃𝑝 ∈
ℙ ∃𝑞 ∈
ℙ ∃𝑟 ∈
ℙ ((𝑝 ∈ Odd
∧ 𝑞 ∈ Odd ∧
𝑟 ∈ Odd ) ∧ 𝑧 = ((𝑝 + 𝑞) + 𝑟))} |