Detailed syntax breakdown of Definition df-prpr
Step | Hyp | Ref
| Expression |
1 | | cprpr 44637 |
. 2
class
Pairsproper |
2 | | vv |
. . 3
setvar 𝑣 |
3 | | cvv 3408 |
. . 3
class
V |
4 | | va |
. . . . . . . . 9
setvar 𝑎 |
5 | 4 | cv 1542 |
. . . . . . . 8
class 𝑎 |
6 | | vb |
. . . . . . . . 9
setvar 𝑏 |
7 | 6 | cv 1542 |
. . . . . . . 8
class 𝑏 |
8 | 5, 7 | wne 2940 |
. . . . . . 7
wff 𝑎 ≠ 𝑏 |
9 | | vp |
. . . . . . . . 9
setvar 𝑝 |
10 | 9 | cv 1542 |
. . . . . . . 8
class 𝑝 |
11 | 5, 7 | cpr 4543 |
. . . . . . . 8
class {𝑎, 𝑏} |
12 | 10, 11 | wceq 1543 |
. . . . . . 7
wff 𝑝 = {𝑎, 𝑏} |
13 | 8, 12 | wa 399 |
. . . . . 6
wff (𝑎 ≠ 𝑏 ∧ 𝑝 = {𝑎, 𝑏}) |
14 | 2 | cv 1542 |
. . . . . 6
class 𝑣 |
15 | 13, 6, 14 | wrex 3062 |
. . . . 5
wff
∃𝑏 ∈
𝑣 (𝑎 ≠ 𝑏 ∧ 𝑝 = {𝑎, 𝑏}) |
16 | 15, 4, 14 | wrex 3062 |
. . . 4
wff
∃𝑎 ∈
𝑣 ∃𝑏 ∈ 𝑣 (𝑎 ≠ 𝑏 ∧ 𝑝 = {𝑎, 𝑏}) |
17 | 16, 9 | cab 2714 |
. . 3
class {𝑝 ∣ ∃𝑎 ∈ 𝑣 ∃𝑏 ∈ 𝑣 (𝑎 ≠ 𝑏 ∧ 𝑝 = {𝑎, 𝑏})} |
18 | 2, 3, 17 | cmpt 5135 |
. 2
class (𝑣 ∈ V ↦ {𝑝 ∣ ∃𝑎 ∈ 𝑣 ∃𝑏 ∈ 𝑣 (𝑎 ≠ 𝑏 ∧ 𝑝 = {𝑎, 𝑏})}) |
19 | 1, 18 | wceq 1543 |
1
wff
Pairsproper = (𝑣 ∈ V ↦ {𝑝 ∣ ∃𝑎 ∈ 𝑣 ∃𝑏 ∈ 𝑣 (𝑎 ≠ 𝑏 ∧ 𝑝 = {𝑎, 𝑏})}) |