Step | Hyp | Ref
| Expression |
1 | | df-iota 6297 |
. 2
⊢
(℩𝑥𝜑) = ∪
{𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}} |
2 | | abeq1 2865 |
. . . . 5
⊢ ({𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}} = ∪ {𝑧 ∣ ∃𝑤(𝑧 = {𝑥 ∣ 𝜑} ∧ 𝑧 = {𝑤})} ↔ ∀𝑦({𝑥 ∣ 𝜑} = {𝑦} ↔ 𝑦 ∈ ∪ {𝑧 ∣ ∃𝑤(𝑧 = {𝑥 ∣ 𝜑} ∧ 𝑧 = {𝑤})})) |
3 | | exdistr 1962 |
. . . . . 6
⊢
(∃𝑧∃𝑤(𝑦 ∈ 𝑧 ∧ (𝑧 = {𝑥 ∣ 𝜑} ∧ 𝑧 = {𝑤})) ↔ ∃𝑧(𝑦 ∈ 𝑧 ∧ ∃𝑤(𝑧 = {𝑥 ∣ 𝜑} ∧ 𝑧 = {𝑤}))) |
4 | | vex 3402 |
. . . . . . . . 9
⊢ 𝑦 ∈ V |
5 | | sneq 4526 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑦 → {𝑤} = {𝑦}) |
6 | 5 | eqeq2d 2749 |
. . . . . . . . 9
⊢ (𝑤 = 𝑦 → ({𝑥 ∣ 𝜑} = {𝑤} ↔ {𝑥 ∣ 𝜑} = {𝑦})) |
7 | 4, 6 | ceqsexv 3445 |
. . . . . . . 8
⊢
(∃𝑤(𝑤 = 𝑦 ∧ {𝑥 ∣ 𝜑} = {𝑤}) ↔ {𝑥 ∣ 𝜑} = {𝑦}) |
8 | | snex 5298 |
. . . . . . . . . . 11
⊢ {𝑤} ∈ V |
9 | | eqeq1 2742 |
. . . . . . . . . . . . 13
⊢ (𝑧 = {𝑤} → (𝑧 = {𝑥 ∣ 𝜑} ↔ {𝑤} = {𝑥 ∣ 𝜑})) |
10 | | eleq2 2821 |
. . . . . . . . . . . . 13
⊢ (𝑧 = {𝑤} → (𝑦 ∈ 𝑧 ↔ 𝑦 ∈ {𝑤})) |
11 | 9, 10 | anbi12d 634 |
. . . . . . . . . . . 12
⊢ (𝑧 = {𝑤} → ((𝑧 = {𝑥 ∣ 𝜑} ∧ 𝑦 ∈ 𝑧) ↔ ({𝑤} = {𝑥 ∣ 𝜑} ∧ 𝑦 ∈ {𝑤}))) |
12 | | eqcom 2745 |
. . . . . . . . . . . . 13
⊢ ({𝑤} = {𝑥 ∣ 𝜑} ↔ {𝑥 ∣ 𝜑} = {𝑤}) |
13 | | velsn 4532 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ {𝑤} ↔ 𝑦 = 𝑤) |
14 | | equcom 2030 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑤 ↔ 𝑤 = 𝑦) |
15 | 13, 14 | bitri 278 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ {𝑤} ↔ 𝑤 = 𝑦) |
16 | 12, 15 | anbi12ci 631 |
. . . . . . . . . . . 12
⊢ (({𝑤} = {𝑥 ∣ 𝜑} ∧ 𝑦 ∈ {𝑤}) ↔ (𝑤 = 𝑦 ∧ {𝑥 ∣ 𝜑} = {𝑤})) |
17 | 11, 16 | bitrdi 290 |
. . . . . . . . . . 11
⊢ (𝑧 = {𝑤} → ((𝑧 = {𝑥 ∣ 𝜑} ∧ 𝑦 ∈ 𝑧) ↔ (𝑤 = 𝑦 ∧ {𝑥 ∣ 𝜑} = {𝑤}))) |
18 | 8, 17 | ceqsexv 3445 |
. . . . . . . . . 10
⊢
(∃𝑧(𝑧 = {𝑤} ∧ (𝑧 = {𝑥 ∣ 𝜑} ∧ 𝑦 ∈ 𝑧)) ↔ (𝑤 = 𝑦 ∧ {𝑥 ∣ 𝜑} = {𝑤})) |
19 | | an13 647 |
. . . . . . . . . . 11
⊢ ((𝑧 = {𝑤} ∧ (𝑧 = {𝑥 ∣ 𝜑} ∧ 𝑦 ∈ 𝑧)) ↔ (𝑦 ∈ 𝑧 ∧ (𝑧 = {𝑥 ∣ 𝜑} ∧ 𝑧 = {𝑤}))) |
20 | 19 | exbii 1854 |
. . . . . . . . . 10
⊢
(∃𝑧(𝑧 = {𝑤} ∧ (𝑧 = {𝑥 ∣ 𝜑} ∧ 𝑦 ∈ 𝑧)) ↔ ∃𝑧(𝑦 ∈ 𝑧 ∧ (𝑧 = {𝑥 ∣ 𝜑} ∧ 𝑧 = {𝑤}))) |
21 | 18, 20 | bitr3i 280 |
. . . . . . . . 9
⊢ ((𝑤 = 𝑦 ∧ {𝑥 ∣ 𝜑} = {𝑤}) ↔ ∃𝑧(𝑦 ∈ 𝑧 ∧ (𝑧 = {𝑥 ∣ 𝜑} ∧ 𝑧 = {𝑤}))) |
22 | 21 | exbii 1854 |
. . . . . . . 8
⊢
(∃𝑤(𝑤 = 𝑦 ∧ {𝑥 ∣ 𝜑} = {𝑤}) ↔ ∃𝑤∃𝑧(𝑦 ∈ 𝑧 ∧ (𝑧 = {𝑥 ∣ 𝜑} ∧ 𝑧 = {𝑤}))) |
23 | 7, 22 | bitr3i 280 |
. . . . . . 7
⊢ ({𝑥 ∣ 𝜑} = {𝑦} ↔ ∃𝑤∃𝑧(𝑦 ∈ 𝑧 ∧ (𝑧 = {𝑥 ∣ 𝜑} ∧ 𝑧 = {𝑤}))) |
24 | | excom 2170 |
. . . . . . 7
⊢
(∃𝑤∃𝑧(𝑦 ∈ 𝑧 ∧ (𝑧 = {𝑥 ∣ 𝜑} ∧ 𝑧 = {𝑤})) ↔ ∃𝑧∃𝑤(𝑦 ∈ 𝑧 ∧ (𝑧 = {𝑥 ∣ 𝜑} ∧ 𝑧 = {𝑤}))) |
25 | 23, 24 | bitri 278 |
. . . . . 6
⊢ ({𝑥 ∣ 𝜑} = {𝑦} ↔ ∃𝑧∃𝑤(𝑦 ∈ 𝑧 ∧ (𝑧 = {𝑥 ∣ 𝜑} ∧ 𝑧 = {𝑤}))) |
26 | | eluniab 4811 |
. . . . . 6
⊢ (𝑦 ∈ ∪ {𝑧
∣ ∃𝑤(𝑧 = {𝑥 ∣ 𝜑} ∧ 𝑧 = {𝑤})} ↔ ∃𝑧(𝑦 ∈ 𝑧 ∧ ∃𝑤(𝑧 = {𝑥 ∣ 𝜑} ∧ 𝑧 = {𝑤}))) |
27 | 3, 25, 26 | 3bitr4i 306 |
. . . . 5
⊢ ({𝑥 ∣ 𝜑} = {𝑦} ↔ 𝑦 ∈ ∪ {𝑧 ∣ ∃𝑤(𝑧 = {𝑥 ∣ 𝜑} ∧ 𝑧 = {𝑤})}) |
28 | 2, 27 | mpgbir 1806 |
. . . 4
⊢ {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}} = ∪ {𝑧 ∣ ∃𝑤(𝑧 = {𝑥 ∣ 𝜑} ∧ 𝑧 = {𝑤})} |
29 | | df-sn 4517 |
. . . . . . 7
⊢ {{𝑥 ∣ 𝜑}} = {𝑧 ∣ 𝑧 = {𝑥 ∣ 𝜑}} |
30 | | dfsingles2 33861 |
. . . . . . 7
⊢ Singletons = {𝑧 ∣ ∃𝑤 𝑧 = {𝑤}} |
31 | 29, 30 | ineq12i 4101 |
. . . . . 6
⊢ ({{𝑥 ∣ 𝜑}} ∩ Singletons
) = ({𝑧 ∣
𝑧 = {𝑥 ∣ 𝜑}} ∩ {𝑧 ∣ ∃𝑤 𝑧 = {𝑤}}) |
32 | | inab 4189 |
. . . . . . 7
⊢ ({𝑧 ∣ 𝑧 = {𝑥 ∣ 𝜑}} ∩ {𝑧 ∣ ∃𝑤 𝑧 = {𝑤}}) = {𝑧 ∣ (𝑧 = {𝑥 ∣ 𝜑} ∧ ∃𝑤 𝑧 = {𝑤})} |
33 | | 19.42v 1961 |
. . . . . . . . 9
⊢
(∃𝑤(𝑧 = {𝑥 ∣ 𝜑} ∧ 𝑧 = {𝑤}) ↔ (𝑧 = {𝑥 ∣ 𝜑} ∧ ∃𝑤 𝑧 = {𝑤})) |
34 | 33 | bicomi 227 |
. . . . . . . 8
⊢ ((𝑧 = {𝑥 ∣ 𝜑} ∧ ∃𝑤 𝑧 = {𝑤}) ↔ ∃𝑤(𝑧 = {𝑥 ∣ 𝜑} ∧ 𝑧 = {𝑤})) |
35 | 34 | abbii 2803 |
. . . . . . 7
⊢ {𝑧 ∣ (𝑧 = {𝑥 ∣ 𝜑} ∧ ∃𝑤 𝑧 = {𝑤})} = {𝑧 ∣ ∃𝑤(𝑧 = {𝑥 ∣ 𝜑} ∧ 𝑧 = {𝑤})} |
36 | 32, 35 | eqtri 2761 |
. . . . . 6
⊢ ({𝑧 ∣ 𝑧 = {𝑥 ∣ 𝜑}} ∩ {𝑧 ∣ ∃𝑤 𝑧 = {𝑤}}) = {𝑧 ∣ ∃𝑤(𝑧 = {𝑥 ∣ 𝜑} ∧ 𝑧 = {𝑤})} |
37 | 31, 36 | eqtri 2761 |
. . . . 5
⊢ ({{𝑥 ∣ 𝜑}} ∩ Singletons
) = {𝑧 ∣
∃𝑤(𝑧 = {𝑥 ∣ 𝜑} ∧ 𝑧 = {𝑤})} |
38 | 37 | unieqi 4809 |
. . . 4
⊢ ∪ ({{𝑥
∣ 𝜑}} ∩ Singletons ) = ∪ {𝑧 ∣ ∃𝑤(𝑧 = {𝑥 ∣ 𝜑} ∧ 𝑧 = {𝑤})} |
39 | 28, 38 | eqtr4i 2764 |
. . 3
⊢ {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}} = ∪ ({{𝑥 ∣ 𝜑}} ∩ Singletons
) |
40 | 39 | unieqi 4809 |
. 2
⊢ ∪ {𝑦
∣ {𝑥 ∣ 𝜑} = {𝑦}} = ∪ ∪ ({{𝑥
∣ 𝜑}} ∩ Singletons ) |
41 | 1, 40 | eqtri 2761 |
1
⊢
(℩𝑥𝜑) = ∪
∪ ({{𝑥 ∣ 𝜑}} ∩ Singletons
) |