| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | df-iota 6514 | . 2
⊢
(℩𝑥𝜑) = ∪
{𝑤 ∣ {𝑥 ∣ 𝜑} = {𝑤}} | 
| 2 |  | n0 4353 | . . . 4
⊢ (∪ {𝑤
∣ {𝑥 ∣ 𝜑} = {𝑤}} ≠ ∅ ↔ ∃𝑣 𝑣 ∈ ∪ {𝑤 ∣ {𝑥 ∣ 𝜑} = {𝑤}}) | 
| 3 |  | eluni 4910 | . . . . . 6
⊢ (𝑣 ∈ ∪ {𝑤
∣ {𝑥 ∣ 𝜑} = {𝑤}} ↔ ∃𝑦(𝑣 ∈ 𝑦 ∧ 𝑦 ∈ {𝑤 ∣ {𝑥 ∣ 𝜑} = {𝑤}})) | 
| 4 |  | vex 3484 | . . . . . . . . . 10
⊢ 𝑦 ∈ V | 
| 5 |  | sneq 4636 | . . . . . . . . . . 11
⊢ (𝑤 = 𝑦 → {𝑤} = {𝑦}) | 
| 6 | 5 | eqeq2d 2748 | . . . . . . . . . 10
⊢ (𝑤 = 𝑦 → ({𝑥 ∣ 𝜑} = {𝑤} ↔ {𝑥 ∣ 𝜑} = {𝑦})) | 
| 7 | 4, 6 | elab 3679 | . . . . . . . . 9
⊢ (𝑦 ∈ {𝑤 ∣ {𝑥 ∣ 𝜑} = {𝑤}} ↔ {𝑥 ∣ 𝜑} = {𝑦}) | 
| 8 | 7 | biimpi 216 | . . . . . . . 8
⊢ (𝑦 ∈ {𝑤 ∣ {𝑥 ∣ 𝜑} = {𝑤}} → {𝑥 ∣ 𝜑} = {𝑦}) | 
| 9 | 8 | adantl 481 | . . . . . . 7
⊢ ((𝑣 ∈ 𝑦 ∧ 𝑦 ∈ {𝑤 ∣ {𝑥 ∣ 𝜑} = {𝑤}}) → {𝑥 ∣ 𝜑} = {𝑦}) | 
| 10 | 9 | eximi 1835 | . . . . . 6
⊢
(∃𝑦(𝑣 ∈ 𝑦 ∧ 𝑦 ∈ {𝑤 ∣ {𝑥 ∣ 𝜑} = {𝑤}}) → ∃𝑦{𝑥 ∣ 𝜑} = {𝑦}) | 
| 11 | 3, 10 | sylbi 217 | . . . . 5
⊢ (𝑣 ∈ ∪ {𝑤
∣ {𝑥 ∣ 𝜑} = {𝑤}} → ∃𝑦{𝑥 ∣ 𝜑} = {𝑦}) | 
| 12 | 11 | exlimiv 1930 | . . . 4
⊢
(∃𝑣 𝑣 ∈ ∪ {𝑤
∣ {𝑥 ∣ 𝜑} = {𝑤}} → ∃𝑦{𝑥 ∣ 𝜑} = {𝑦}) | 
| 13 | 2, 12 | sylbi 217 | . . 3
⊢ (∪ {𝑤
∣ {𝑥 ∣ 𝜑} = {𝑤}} ≠ ∅ → ∃𝑦{𝑥 ∣ 𝜑} = {𝑦}) | 
| 14 | 13 | necon1bi 2969 | . 2
⊢ (¬
∃𝑦{𝑥 ∣ 𝜑} = {𝑦} → ∪ {𝑤 ∣ {𝑥 ∣ 𝜑} = {𝑤}} = ∅) | 
| 15 | 1, 14 | eqtrid 2789 | 1
⊢ (¬
∃𝑦{𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) = ∅) |