Detailed syntax breakdown of Definition df-wun
Step | Hyp | Ref
| Expression |
1 | | cwun 10314 |
. 2
class
WUni |
2 | | vu |
. . . . . 6
setvar 𝑢 |
3 | 2 | cv 1542 |
. . . . 5
class 𝑢 |
4 | 3 | wtr 5161 |
. . . 4
wff Tr 𝑢 |
5 | | c0 4237 |
. . . . 5
class
∅ |
6 | 3, 5 | wne 2940 |
. . . 4
wff 𝑢 ≠ ∅ |
7 | | vx |
. . . . . . . . 9
setvar 𝑥 |
8 | 7 | cv 1542 |
. . . . . . . 8
class 𝑥 |
9 | 8 | cuni 4819 |
. . . . . . 7
class ∪ 𝑥 |
10 | 9, 3 | wcel 2110 |
. . . . . 6
wff ∪ 𝑥
∈ 𝑢 |
11 | 8 | cpw 4513 |
. . . . . . 7
class 𝒫
𝑥 |
12 | 11, 3 | wcel 2110 |
. . . . . 6
wff 𝒫
𝑥 ∈ 𝑢 |
13 | | vy |
. . . . . . . . . 10
setvar 𝑦 |
14 | 13 | cv 1542 |
. . . . . . . . 9
class 𝑦 |
15 | 8, 14 | cpr 4543 |
. . . . . . . 8
class {𝑥, 𝑦} |
16 | 15, 3 | wcel 2110 |
. . . . . . 7
wff {𝑥, 𝑦} ∈ 𝑢 |
17 | 16, 13, 3 | wral 3061 |
. . . . . 6
wff
∀𝑦 ∈
𝑢 {𝑥, 𝑦} ∈ 𝑢 |
18 | 10, 12, 17 | w3a 1089 |
. . . . 5
wff (∪ 𝑥
∈ 𝑢 ∧ 𝒫
𝑥 ∈ 𝑢 ∧ ∀𝑦 ∈ 𝑢 {𝑥, 𝑦} ∈ 𝑢) |
19 | 18, 7, 3 | wral 3061 |
. . . 4
wff
∀𝑥 ∈
𝑢 (∪ 𝑥
∈ 𝑢 ∧ 𝒫
𝑥 ∈ 𝑢 ∧ ∀𝑦 ∈ 𝑢 {𝑥, 𝑦} ∈ 𝑢) |
20 | 4, 6, 19 | w3a 1089 |
. . 3
wff (Tr 𝑢 ∧ 𝑢 ≠ ∅ ∧ ∀𝑥 ∈ 𝑢 (∪ 𝑥 ∈ 𝑢 ∧ 𝒫 𝑥 ∈ 𝑢 ∧ ∀𝑦 ∈ 𝑢 {𝑥, 𝑦} ∈ 𝑢)) |
21 | 20, 2 | cab 2714 |
. 2
class {𝑢 ∣ (Tr 𝑢 ∧ 𝑢 ≠ ∅ ∧ ∀𝑥 ∈ 𝑢 (∪ 𝑥 ∈ 𝑢 ∧ 𝒫 𝑥 ∈ 𝑢 ∧ ∀𝑦 ∈ 𝑢 {𝑥, 𝑦} ∈ 𝑢))} |
22 | 1, 21 | wceq 1543 |
1
wff WUni =
{𝑢 ∣ (Tr 𝑢 ∧ 𝑢 ≠ ∅ ∧ ∀𝑥 ∈ 𝑢 (∪ 𝑥 ∈ 𝑢 ∧ 𝒫 𝑥 ∈ 𝑢 ∧ ∀𝑦 ∈ 𝑢 {𝑥, 𝑦} ∈ 𝑢))} |