Detailed syntax breakdown of Definition df-spr
Step | Hyp | Ref
| Expression |
1 | | cspr 44492 |
. 2
class
Pairs |
2 | | vv |
. . 3
setvar 𝑣 |
3 | | cvv 3398 |
. . 3
class
V |
4 | | vp |
. . . . . . . 8
setvar 𝑝 |
5 | 4 | cv 1541 |
. . . . . . 7
class 𝑝 |
6 | | va |
. . . . . . . . 9
setvar 𝑎 |
7 | 6 | cv 1541 |
. . . . . . . 8
class 𝑎 |
8 | | vb |
. . . . . . . . 9
setvar 𝑏 |
9 | 8 | cv 1541 |
. . . . . . . 8
class 𝑏 |
10 | 7, 9 | cpr 4518 |
. . . . . . 7
class {𝑎, 𝑏} |
11 | 5, 10 | wceq 1542 |
. . . . . 6
wff 𝑝 = {𝑎, 𝑏} |
12 | 2 | cv 1541 |
. . . . . 6
class 𝑣 |
13 | 11, 8, 12 | wrex 3054 |
. . . . 5
wff
∃𝑏 ∈
𝑣 𝑝 = {𝑎, 𝑏} |
14 | 13, 6, 12 | wrex 3054 |
. . . 4
wff
∃𝑎 ∈
𝑣 ∃𝑏 ∈ 𝑣 𝑝 = {𝑎, 𝑏} |
15 | 14, 4 | cab 2716 |
. . 3
class {𝑝 ∣ ∃𝑎 ∈ 𝑣 ∃𝑏 ∈ 𝑣 𝑝 = {𝑎, 𝑏}} |
16 | 2, 3, 15 | cmpt 5110 |
. 2
class (𝑣 ∈ V ↦ {𝑝 ∣ ∃𝑎 ∈ 𝑣 ∃𝑏 ∈ 𝑣 𝑝 = {𝑎, 𝑏}}) |
17 | 1, 16 | wceq 1542 |
1
wff Pairs =
(𝑣 ∈ V ↦ {𝑝 ∣ ∃𝑎 ∈ 𝑣 ∃𝑏 ∈ 𝑣 𝑝 = {𝑎, 𝑏}}) |