Step | Hyp | Ref
| Expression |
1 | | df-iota 4810 |
. 2
⊢
(℩xφ) = ∪ {y ∣ {x
∣ φ} = {y}} |
2 | | unieq 3580 |
. . . . . . . 8
⊢
({x ∣ φ} = {y}
→ ∪ {x
∣ φ} = ∪ {y}) |
3 | | vex 2554 |
. . . . . . . . 9
⊢ y ∈
V |
4 | 3 | unisn 3587 |
. . . . . . . 8
⊢ ∪ {y} = y |
5 | 2, 4 | syl6eq 2085 |
. . . . . . 7
⊢
({x ∣ φ} = {y}
→ ∪ {x
∣ φ} = y) |
6 | | df-pw 3353 |
. . . . . . . . . . 11
⊢ 𝒫
A = {x
∣ x ⊆ A} |
7 | 6 | sseq2i 2964 |
. . . . . . . . . 10
⊢
({x ∣ φ} ⊆ 𝒫 A ↔ {x
∣ φ} ⊆ {x ∣ x
⊆ A}) |
8 | | ss2ab 3002 |
. . . . . . . . . 10
⊢
({x ∣ φ} ⊆ {x ∣ x
⊆ A} ↔ ∀x(φ → x ⊆ A)) |
9 | 7, 8 | bitri 173 |
. . . . . . . . 9
⊢
({x ∣ φ} ⊆ 𝒫 A ↔ ∀x(φ → x ⊆ A)) |
10 | 9 | biimpri 124 |
. . . . . . . 8
⊢ (∀x(φ → x ⊆ A)
→ {x ∣ φ} ⊆ 𝒫 A) |
11 | | sspwuni 3730 |
. . . . . . . 8
⊢
({x ∣ φ} ⊆ 𝒫 A ↔ ∪ {x ∣ φ}
⊆ A) |
12 | 10, 11 | sylib 127 |
. . . . . . 7
⊢ (∀x(φ → x ⊆ A)
→ ∪ {x
∣ φ} ⊆ A) |
13 | | sseq1 2960 |
. . . . . . . 8
⊢ (∪ {x ∣ φ} = y
→ (∪ {x
∣ φ} ⊆ A ↔ y
⊆ A)) |
14 | 13 | biimpa 280 |
. . . . . . 7
⊢ ((∪ {x ∣ φ} = y
∧ ∪ {x ∣ φ}
⊆ A) → y ⊆ A) |
15 | 5, 12, 14 | syl2anr 274 |
. . . . . 6
⊢ ((∀x(φ → x ⊆ A)
∧ {x
∣ φ} = {y}) → y
⊆ A) |
16 | 15 | ex 108 |
. . . . 5
⊢ (∀x(φ → x ⊆ A)
→ ({x ∣ φ} = {y}
→ y ⊆ A)) |
17 | 16 | ss2abdv 3007 |
. . . 4
⊢ (∀x(φ → x ⊆ A)
→ {y ∣ {x ∣ φ}
= {y}} ⊆ {y ∣ y
⊆ A}) |
18 | | df-pw 3353 |
. . . 4
⊢ 𝒫
A = {y
∣ y ⊆ A} |
19 | 17, 18 | syl6sseqr 2986 |
. . 3
⊢ (∀x(φ → x ⊆ A)
→ {y ∣ {x ∣ φ}
= {y}} ⊆ 𝒫 A) |
20 | | sspwuni 3730 |
. . 3
⊢
({y ∣ {x ∣ φ}
= {y}} ⊆ 𝒫 A ↔ ∪ {y ∣ {x
∣ φ} = {y}} ⊆ A) |
21 | 19, 20 | sylib 127 |
. 2
⊢ (∀x(φ → x ⊆ A)
→ ∪ {y
∣ {x ∣ φ} = {y}}
⊆ A) |
22 | 1, 21 | syl5eqss 2983 |
1
⊢ (∀x(φ → x ⊆ A)
→ (℩xφ) ⊆ A) |