Detailed syntax breakdown of Definition df-ref
Step | Hyp | Ref
| Expression |
1 | | cref 22399 |
. 2
class
Ref |
2 | | vy |
. . . . . . 7
setvar 𝑦 |
3 | 2 | cv 1542 |
. . . . . 6
class 𝑦 |
4 | 3 | cuni 4819 |
. . . . 5
class ∪ 𝑦 |
5 | | vx |
. . . . . . 7
setvar 𝑥 |
6 | 5 | cv 1542 |
. . . . . 6
class 𝑥 |
7 | 6 | cuni 4819 |
. . . . 5
class ∪ 𝑥 |
8 | 4, 7 | wceq 1543 |
. . . 4
wff ∪ 𝑦 =
∪ 𝑥 |
9 | | vz |
. . . . . . . 8
setvar 𝑧 |
10 | 9 | cv 1542 |
. . . . . . 7
class 𝑧 |
11 | | vw |
. . . . . . . 8
setvar 𝑤 |
12 | 11 | cv 1542 |
. . . . . . 7
class 𝑤 |
13 | 10, 12 | wss 3866 |
. . . . . 6
wff 𝑧 ⊆ 𝑤 |
14 | 13, 11, 3 | wrex 3062 |
. . . . 5
wff
∃𝑤 ∈
𝑦 𝑧 ⊆ 𝑤 |
15 | 14, 9, 6 | wral 3061 |
. . . 4
wff
∀𝑧 ∈
𝑥 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 |
16 | 8, 15 | wa 399 |
. . 3
wff (∪ 𝑦 =
∪ 𝑥 ∧ ∀𝑧 ∈ 𝑥 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤) |
17 | 16, 5, 2 | copab 5115 |
. 2
class
{〈𝑥, 𝑦〉 ∣ (∪ 𝑦 =
∪ 𝑥 ∧ ∀𝑧 ∈ 𝑥 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)} |
18 | 1, 17 | wceq 1543 |
1
wff Ref =
{〈𝑥, 𝑦〉 ∣ (∪ 𝑦 =
∪ 𝑥 ∧ ∀𝑧 ∈ 𝑥 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)} |