Step | Hyp | Ref
| Expression |
1 | | df-iota 5178 |
. 2
⊢
(℩𝑥𝜑) = ∪
{𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}} |
2 | | unieq 3818 |
. . . . . . . 8
⊢ ({𝑥 ∣ 𝜑} = {𝑦} → ∪ {𝑥 ∣ 𝜑} = ∪ {𝑦}) |
3 | | vex 2740 |
. . . . . . . . 9
⊢ 𝑦 ∈ V |
4 | 3 | unisn 3825 |
. . . . . . . 8
⊢ ∪ {𝑦}
= 𝑦 |
5 | 2, 4 | eqtrdi 2226 |
. . . . . . 7
⊢ ({𝑥 ∣ 𝜑} = {𝑦} → ∪ {𝑥 ∣ 𝜑} = 𝑦) |
6 | | df-pw 3577 |
. . . . . . . . . . 11
⊢ 𝒫
𝐴 = {𝑥 ∣ 𝑥 ⊆ 𝐴} |
7 | 6 | sseq2i 3182 |
. . . . . . . . . 10
⊢ ({𝑥 ∣ 𝜑} ⊆ 𝒫 𝐴 ↔ {𝑥 ∣ 𝜑} ⊆ {𝑥 ∣ 𝑥 ⊆ 𝐴}) |
8 | | ss2ab 3223 |
. . . . . . . . . 10
⊢ ({𝑥 ∣ 𝜑} ⊆ {𝑥 ∣ 𝑥 ⊆ 𝐴} ↔ ∀𝑥(𝜑 → 𝑥 ⊆ 𝐴)) |
9 | 7, 8 | bitri 184 |
. . . . . . . . 9
⊢ ({𝑥 ∣ 𝜑} ⊆ 𝒫 𝐴 ↔ ∀𝑥(𝜑 → 𝑥 ⊆ 𝐴)) |
10 | 9 | biimpri 133 |
. . . . . . . 8
⊢
(∀𝑥(𝜑 → 𝑥 ⊆ 𝐴) → {𝑥 ∣ 𝜑} ⊆ 𝒫 𝐴) |
11 | | sspwuni 3971 |
. . . . . . . 8
⊢ ({𝑥 ∣ 𝜑} ⊆ 𝒫 𝐴 ↔ ∪ {𝑥 ∣ 𝜑} ⊆ 𝐴) |
12 | 10, 11 | sylib 122 |
. . . . . . 7
⊢
(∀𝑥(𝜑 → 𝑥 ⊆ 𝐴) → ∪ {𝑥 ∣ 𝜑} ⊆ 𝐴) |
13 | | sseq1 3178 |
. . . . . . . 8
⊢ (∪ {𝑥
∣ 𝜑} = 𝑦 → (∪ {𝑥
∣ 𝜑} ⊆ 𝐴 ↔ 𝑦 ⊆ 𝐴)) |
14 | 13 | biimpa 296 |
. . . . . . 7
⊢ ((∪ {𝑥
∣ 𝜑} = 𝑦 ∧ ∪ {𝑥
∣ 𝜑} ⊆ 𝐴) → 𝑦 ⊆ 𝐴) |
15 | 5, 12, 14 | syl2anr 290 |
. . . . . 6
⊢
((∀𝑥(𝜑 → 𝑥 ⊆ 𝐴) ∧ {𝑥 ∣ 𝜑} = {𝑦}) → 𝑦 ⊆ 𝐴) |
16 | 15 | ex 115 |
. . . . 5
⊢
(∀𝑥(𝜑 → 𝑥 ⊆ 𝐴) → ({𝑥 ∣ 𝜑} = {𝑦} → 𝑦 ⊆ 𝐴)) |
17 | 16 | ss2abdv 3228 |
. . . 4
⊢
(∀𝑥(𝜑 → 𝑥 ⊆ 𝐴) → {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}} ⊆ {𝑦 ∣ 𝑦 ⊆ 𝐴}) |
18 | | df-pw 3577 |
. . . 4
⊢ 𝒫
𝐴 = {𝑦 ∣ 𝑦 ⊆ 𝐴} |
19 | 17, 18 | sseqtrrdi 3204 |
. . 3
⊢
(∀𝑥(𝜑 → 𝑥 ⊆ 𝐴) → {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}} ⊆ 𝒫 𝐴) |
20 | | sspwuni 3971 |
. . 3
⊢ ({𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}} ⊆ 𝒫 𝐴 ↔ ∪ {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}} ⊆ 𝐴) |
21 | 19, 20 | sylib 122 |
. 2
⊢
(∀𝑥(𝜑 → 𝑥 ⊆ 𝐴) → ∪ {𝑦 ∣ {𝑥 ∣ 𝜑} = {𝑦}} ⊆ 𝐴) |
22 | 1, 21 | eqsstrid 3201 |
1
⊢
(∀𝑥(𝜑 → 𝑥 ⊆ 𝐴) → (℩𝑥𝜑) ⊆ 𝐴) |