Step | Hyp | Ref
| Expression |
1 | | dfiota2 5138 |
. 2
⊢
(℩𝑥𝜑) = ∪
{𝑧 ∣ ∀𝑥(𝜑 ↔ 𝑥 = 𝑧)} |
2 | | vex 2715 |
. . . . . . 7
⊢ 𝑦 ∈ V |
3 | | sbeqalb 2993 |
. . . . . . . 8
⊢ (𝑦 ∈ V → ((∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ∧ ∀𝑥(𝜑 ↔ 𝑥 = 𝑧)) → 𝑦 = 𝑧)) |
4 | | equcomi 1684 |
. . . . . . . 8
⊢ (𝑦 = 𝑧 → 𝑧 = 𝑦) |
5 | 3, 4 | syl6 33 |
. . . . . . 7
⊢ (𝑦 ∈ V → ((∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ∧ ∀𝑥(𝜑 ↔ 𝑥 = 𝑧)) → 𝑧 = 𝑦)) |
6 | 2, 5 | ax-mp 5 |
. . . . . 6
⊢
((∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ∧ ∀𝑥(𝜑 ↔ 𝑥 = 𝑧)) → 𝑧 = 𝑦) |
7 | 6 | ex 114 |
. . . . 5
⊢
(∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → (∀𝑥(𝜑 ↔ 𝑥 = 𝑧) → 𝑧 = 𝑦)) |
8 | | equequ2 1693 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑧 → (𝑥 = 𝑦 ↔ 𝑥 = 𝑧)) |
9 | 8 | equcoms 1688 |
. . . . . . . . 9
⊢ (𝑧 = 𝑦 → (𝑥 = 𝑦 ↔ 𝑥 = 𝑧)) |
10 | 9 | bibi2d 231 |
. . . . . . . 8
⊢ (𝑧 = 𝑦 → ((𝜑 ↔ 𝑥 = 𝑦) ↔ (𝜑 ↔ 𝑥 = 𝑧))) |
11 | 10 | biimpd 143 |
. . . . . . 7
⊢ (𝑧 = 𝑦 → ((𝜑 ↔ 𝑥 = 𝑦) → (𝜑 ↔ 𝑥 = 𝑧))) |
12 | 11 | alimdv 1859 |
. . . . . 6
⊢ (𝑧 = 𝑦 → (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → ∀𝑥(𝜑 ↔ 𝑥 = 𝑧))) |
13 | 12 | com12 30 |
. . . . 5
⊢
(∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → (𝑧 = 𝑦 → ∀𝑥(𝜑 ↔ 𝑥 = 𝑧))) |
14 | 7, 13 | impbid 128 |
. . . 4
⊢
(∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → (∀𝑥(𝜑 ↔ 𝑥 = 𝑧) ↔ 𝑧 = 𝑦)) |
15 | 14 | alrimiv 1854 |
. . 3
⊢
(∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → ∀𝑧(∀𝑥(𝜑 ↔ 𝑥 = 𝑧) ↔ 𝑧 = 𝑦)) |
16 | | uniabio 5147 |
. . 3
⊢
(∀𝑧(∀𝑥(𝜑 ↔ 𝑥 = 𝑧) ↔ 𝑧 = 𝑦) → ∪ {𝑧 ∣ ∀𝑥(𝜑 ↔ 𝑥 = 𝑧)} = 𝑦) |
17 | 15, 16 | syl 14 |
. 2
⊢
(∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → ∪ {𝑧 ∣ ∀𝑥(𝜑 ↔ 𝑥 = 𝑧)} = 𝑦) |
18 | 1, 17 | syl5eq 2202 |
1
⊢
(∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → (℩𝑥𝜑) = 𝑦) |