Detailed syntax breakdown of Definition df-gbe
Step | Hyp | Ref
| Expression |
1 | | cgbe 45197 |
. 2
class
GoldbachEven |
2 | | vp |
. . . . . . . 8
setvar 𝑝 |
3 | 2 | cv 1538 |
. . . . . . 7
class 𝑝 |
4 | | codd 45077 |
. . . . . . 7
class
Odd |
5 | 3, 4 | wcel 2106 |
. . . . . 6
wff 𝑝 ∈ Odd |
6 | | vq |
. . . . . . . 8
setvar 𝑞 |
7 | 6 | cv 1538 |
. . . . . . 7
class 𝑞 |
8 | 7, 4 | wcel 2106 |
. . . . . 6
wff 𝑞 ∈ Odd |
9 | | vz |
. . . . . . . 8
setvar 𝑧 |
10 | 9 | cv 1538 |
. . . . . . 7
class 𝑧 |
11 | | caddc 10874 |
. . . . . . . 8
class
+ |
12 | 3, 7, 11 | co 7275 |
. . . . . . 7
class (𝑝 + 𝑞) |
13 | 10, 12 | wceq 1539 |
. . . . . 6
wff 𝑧 = (𝑝 + 𝑞) |
14 | 5, 8, 13 | w3a 1086 |
. . . . 5
wff (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑧 = (𝑝 + 𝑞)) |
15 | | cprime 16376 |
. . . . 5
class
ℙ |
16 | 14, 6, 15 | wrex 3065 |
. . . 4
wff
∃𝑞 ∈
ℙ (𝑝 ∈ Odd ∧
𝑞 ∈ Odd ∧ 𝑧 = (𝑝 + 𝑞)) |
17 | 16, 2, 15 | wrex 3065 |
. . 3
wff
∃𝑝 ∈
ℙ ∃𝑞 ∈
ℙ (𝑝 ∈ Odd ∧
𝑞 ∈ Odd ∧ 𝑧 = (𝑝 + 𝑞)) |
18 | | ceven 45076 |
. . 3
class
Even |
19 | 17, 9, 18 | crab 3068 |
. 2
class {𝑧 ∈ Even ∣
∃𝑝 ∈ ℙ
∃𝑞 ∈ ℙ
(𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑧 = (𝑝 + 𝑞))} |
20 | 1, 19 | wceq 1539 |
1
wff
GoldbachEven = {𝑧 ∈
Even ∣ ∃𝑝
∈ ℙ ∃𝑞
∈ ℙ (𝑝 ∈
Odd ∧ 𝑞 ∈ Odd
∧ 𝑧 = (𝑝 + 𝑞))} |