Detailed syntax breakdown of Definition df-si
Step | Hyp | Ref
| Expression |
1 | | cA |
. . 3
class A |
2 | 1 | csi 4720 |
. 2
class SI
A |
3 | | vx |
. . . . . . . 8
setvar x |
4 | 3 | cv 1641 |
. . . . . . 7
class x |
5 | | vz |
. . . . . . . . 9
setvar z |
6 | 5 | cv 1641 |
. . . . . . . 8
class z |
7 | 6 | csn 3737 |
. . . . . . 7
class {z} |
8 | 4, 7 | wceq 1642 |
. . . . . 6
wff x =
{z} |
9 | | vy |
. . . . . . . 8
setvar y |
10 | 9 | cv 1641 |
. . . . . . 7
class y |
11 | | vw |
. . . . . . . . 9
setvar w |
12 | 11 | cv 1641 |
. . . . . . . 8
class w |
13 | 12 | csn 3737 |
. . . . . . 7
class {w} |
14 | 10, 13 | wceq 1642 |
. . . . . 6
wff y =
{w} |
15 | 6, 12, 1 | wbr 4639 |
. . . . . 6
wff zAw |
16 | 8, 14, 15 | w3a 934 |
. . . . 5
wff (x
= {z} ∧
y = {w}
∧ zAw) |
17 | 16, 11 | wex 1541 |
. . . 4
wff ∃w(x = {z} ∧ y = {w} ∧ zAw) |
18 | 17, 5 | wex 1541 |
. . 3
wff ∃z∃w(x = {z} ∧ y = {w} ∧ zAw) |
19 | 18, 3, 9 | copab 4622 |
. 2
class {〈x, y〉 ∣ ∃z∃w(x = {z} ∧ y = {w} ∧ zAw)} |
20 | 2, 19 | wceq 1642 |
1
wff SI
A = {〈x, y〉 ∣ ∃z∃w(x = {z} ∧ y = {w} ∧ zAw)} |