Step | Hyp | Ref
| Expression |
1 | | df-iota 6386 |
. 2
⊢
(℩𝑥𝜑) = ∪
{𝑤 ∣ {𝑥 ∣ 𝜑} = {𝑤}} |
2 | | n0 4282 |
. . . 4
⊢ (∪ {𝑤
∣ {𝑥 ∣ 𝜑} = {𝑤}} ≠ ∅ ↔ ∃𝑣 𝑣 ∈ ∪ {𝑤 ∣ {𝑥 ∣ 𝜑} = {𝑤}}) |
3 | | eluni 4844 |
. . . . . 6
⊢ (𝑣 ∈ ∪ {𝑤
∣ {𝑥 ∣ 𝜑} = {𝑤}} ↔ ∃𝑦(𝑣 ∈ 𝑦 ∧ 𝑦 ∈ {𝑤 ∣ {𝑥 ∣ 𝜑} = {𝑤}})) |
4 | | vex 3435 |
. . . . . . . . . 10
⊢ 𝑦 ∈ V |
5 | | sneq 4573 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑦 → {𝑤} = {𝑦}) |
6 | 5 | eqeq2d 2749 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑦 → ({𝑥 ∣ 𝜑} = {𝑤} ↔ {𝑥 ∣ 𝜑} = {𝑦})) |
7 | 4, 6 | elab 3610 |
. . . . . . . . 9
⊢ (𝑦 ∈ {𝑤 ∣ {𝑥 ∣ 𝜑} = {𝑤}} ↔ {𝑥 ∣ 𝜑} = {𝑦}) |
8 | 7 | biimpi 215 |
. . . . . . . 8
⊢ (𝑦 ∈ {𝑤 ∣ {𝑥 ∣ 𝜑} = {𝑤}} → {𝑥 ∣ 𝜑} = {𝑦}) |
9 | 8 | adantl 482 |
. . . . . . 7
⊢ ((𝑣 ∈ 𝑦 ∧ 𝑦 ∈ {𝑤 ∣ {𝑥 ∣ 𝜑} = {𝑤}}) → {𝑥 ∣ 𝜑} = {𝑦}) |
10 | 9 | eximi 1837 |
. . . . . 6
⊢
(∃𝑦(𝑣 ∈ 𝑦 ∧ 𝑦 ∈ {𝑤 ∣ {𝑥 ∣ 𝜑} = {𝑤}}) → ∃𝑦{𝑥 ∣ 𝜑} = {𝑦}) |
11 | 3, 10 | sylbi 216 |
. . . . 5
⊢ (𝑣 ∈ ∪ {𝑤
∣ {𝑥 ∣ 𝜑} = {𝑤}} → ∃𝑦{𝑥 ∣ 𝜑} = {𝑦}) |
12 | 11 | exlimiv 1933 |
. . . 4
⊢
(∃𝑣 𝑣 ∈ ∪ {𝑤
∣ {𝑥 ∣ 𝜑} = {𝑤}} → ∃𝑦{𝑥 ∣ 𝜑} = {𝑦}) |
13 | 2, 12 | sylbi 216 |
. . 3
⊢ (∪ {𝑤
∣ {𝑥 ∣ 𝜑} = {𝑤}} ≠ ∅ → ∃𝑦{𝑥 ∣ 𝜑} = {𝑦}) |
14 | 13 | necon1bi 2972 |
. 2
⊢ (¬
∃𝑦{𝑥 ∣ 𝜑} = {𝑦} → ∪ {𝑤 ∣ {𝑥 ∣ 𝜑} = {𝑤}} = ∅) |
15 | 1, 14 | eqtrid 2790 |
1
⊢ (¬
∃𝑦{𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) = ∅) |