Detailed syntax breakdown of Definition df-sik
Step | Hyp | Ref
| Expression |
1 | | cA |
. . 3
class A |
2 | 1 | csik 4181 |
. 2
class SIk A |
3 | | vx |
. . . . . . . 8
setvar x |
4 | 3 | cv 1641 |
. . . . . . 7
class x |
5 | | vy |
. . . . . . . . 9
setvar y |
6 | 5 | cv 1641 |
. . . . . . . 8
class y |
7 | | vz |
. . . . . . . . 9
setvar z |
8 | 7 | cv 1641 |
. . . . . . . 8
class z |
9 | 6, 8 | copk 4057 |
. . . . . . 7
class ⟪y, z⟫ |
10 | 4, 9 | wceq 1642 |
. . . . . 6
wff x =
⟪y, z⟫ |
11 | | vt |
. . . . . . . . . . . 12
setvar t |
12 | 11 | cv 1641 |
. . . . . . . . . . 11
class t |
13 | 12 | csn 3737 |
. . . . . . . . . 10
class {t} |
14 | 6, 13 | wceq 1642 |
. . . . . . . . 9
wff y =
{t} |
15 | | vu |
. . . . . . . . . . . 12
setvar u |
16 | 15 | cv 1641 |
. . . . . . . . . . 11
class u |
17 | 16 | csn 3737 |
. . . . . . . . . 10
class {u} |
18 | 8, 17 | wceq 1642 |
. . . . . . . . 9
wff z =
{u} |
19 | 12, 16 | copk 4057 |
. . . . . . . . . 10
class ⟪t, u⟫ |
20 | 19, 1 | wcel 1710 |
. . . . . . . . 9
wff ⟪t, u⟫
∈ A |
21 | 14, 18, 20 | w3a 934 |
. . . . . . . 8
wff (y
= {t} ∧
z = {u}
∧ ⟪t, u⟫
∈ A) |
22 | 21, 15 | wex 1541 |
. . . . . . 7
wff ∃u(y = {t} ∧ z = {u} ∧
⟪t, u⟫ ∈
A) |
23 | 22, 11 | wex 1541 |
. . . . . 6
wff ∃t∃u(y = {t} ∧ z = {u} ∧
⟪t, u⟫ ∈
A) |
24 | 10, 23 | wa 358 |
. . . . 5
wff (x
= ⟪y, z⟫ ∧ ∃t∃u(y = {t} ∧ z = {u} ∧
⟪t, u⟫ ∈
A)) |
25 | 24, 7 | wex 1541 |
. . . 4
wff ∃z(x = ⟪y,
z⟫ ∧ ∃t∃u(y = {t} ∧ z = {u} ∧ ⟪t,
u⟫ ∈ A)) |
26 | 25, 5 | wex 1541 |
. . 3
wff ∃y∃z(x = ⟪y,
z⟫ ∧ ∃t∃u(y = {t} ∧ z = {u} ∧ ⟪t,
u⟫ ∈ A)) |
27 | 26, 3 | cab 2339 |
. 2
class {x ∣ ∃y∃z(x = ⟪y,
z⟫ ∧ ∃t∃u(y = {t} ∧ z = {u} ∧ ⟪t,
u⟫ ∈ A))} |
28 | 2, 27 | wceq 1642 |
1
wff SIk A = {x ∣ ∃y∃z(x =
⟪y, z⟫ ∧ ∃t∃u(y = {t} ∧ z = {u} ∧
⟪t, u⟫ ∈
A))} |