Detailed syntax breakdown of Definition df-ext
Step | Hyp | Ref
| Expression |
1 | | cext 5896 |
. 2
class Ext |
2 | | vz |
. . . . . . . . . 10
setvar z |
3 | 2 | cv 1641 |
. . . . . . . . 9
class z |
4 | | vx |
. . . . . . . . . 10
setvar x |
5 | 4 | cv 1641 |
. . . . . . . . 9
class x |
6 | | vr |
. . . . . . . . . 10
setvar r |
7 | 6 | cv 1641 |
. . . . . . . . 9
class r |
8 | 3, 5, 7 | wbr 4639 |
. . . . . . . 8
wff zrx |
9 | | vy |
. . . . . . . . . 10
setvar y |
10 | 9 | cv 1641 |
. . . . . . . . 9
class y |
11 | 3, 10, 7 | wbr 4639 |
. . . . . . . 8
wff zry |
12 | 8, 11 | wb 176 |
. . . . . . 7
wff (zrx ↔ zry) |
13 | | va |
. . . . . . . 8
setvar a |
14 | 13 | cv 1641 |
. . . . . . 7
class a |
15 | 12, 2, 14 | wral 2614 |
. . . . . 6
wff ∀z ∈ a (zrx ↔ zry) |
16 | 4, 9 | weq 1643 |
. . . . . 6
wff x =
y |
17 | 15, 16 | wi 4 |
. . . . 5
wff (∀z ∈ a (zrx ↔ zry) → x =
y) |
18 | 17, 9, 14 | wral 2614 |
. . . 4
wff ∀y ∈ a (∀z ∈ a (zrx ↔ zry) → x =
y) |
19 | 18, 4, 14 | wral 2614 |
. . 3
wff ∀x ∈ a ∀y ∈ a (∀z ∈ a (zrx ↔ zry) → x =
y) |
20 | 19, 6, 13 | copab 4622 |
. 2
class {〈r, a〉 ∣ ∀x ∈ a ∀y ∈ a (∀z ∈ a (zrx ↔
zry) →
x = y)} |
21 | 1, 20 | wceq 1642 |
1
wff Ext =
{〈r,
a〉 ∣ ∀x ∈ a ∀y ∈ a (∀z ∈ a (zrx ↔
zry) →
x = y)} |