| Step | Hyp | Ref
| Expression |
| 1 | | elALT2 5369 |
. . . 4
⊢
∃𝑤 𝑥 ∈ 𝑤 |
| 2 | | ax-nul 5306 |
. . . . 5
⊢
∃𝑧∀𝑥 ¬ 𝑥 ∈ 𝑧 |
| 3 | | elequ1 2115 |
. . . . . . 7
⊢ (𝑥 = 𝑤 → (𝑥 ∈ 𝑧 ↔ 𝑤 ∈ 𝑧)) |
| 4 | 3 | notbid 318 |
. . . . . 6
⊢ (𝑥 = 𝑤 → (¬ 𝑥 ∈ 𝑧 ↔ ¬ 𝑤 ∈ 𝑧)) |
| 5 | 4 | spw 2033 |
. . . . 5
⊢
(∀𝑥 ¬
𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑧) |
| 6 | 2, 5 | eximii 1837 |
. . . 4
⊢
∃𝑧 ¬ 𝑥 ∈ 𝑧 |
| 7 | | exdistrv 1955 |
. . . 4
⊢
(∃𝑤∃𝑧(𝑥 ∈ 𝑤 ∧ ¬ 𝑥 ∈ 𝑧) ↔ (∃𝑤 𝑥 ∈ 𝑤 ∧ ∃𝑧 ¬ 𝑥 ∈ 𝑧)) |
| 8 | 1, 6, 7 | mpbir2an 711 |
. . 3
⊢
∃𝑤∃𝑧(𝑥 ∈ 𝑤 ∧ ¬ 𝑥 ∈ 𝑧) |
| 9 | | ax9v2 2121 |
. . . . . 6
⊢ (𝑤 = 𝑧 → (𝑥 ∈ 𝑤 → 𝑥 ∈ 𝑧)) |
| 10 | 9 | com12 32 |
. . . . 5
⊢ (𝑥 ∈ 𝑤 → (𝑤 = 𝑧 → 𝑥 ∈ 𝑧)) |
| 11 | 10 | con3dimp 408 |
. . . 4
⊢ ((𝑥 ∈ 𝑤 ∧ ¬ 𝑥 ∈ 𝑧) → ¬ 𝑤 = 𝑧) |
| 12 | 11 | 2eximi 1836 |
. . 3
⊢
(∃𝑤∃𝑧(𝑥 ∈ 𝑤 ∧ ¬ 𝑥 ∈ 𝑧) → ∃𝑤∃𝑧 ¬ 𝑤 = 𝑧) |
| 13 | | equequ2 2025 |
. . . . . . 7
⊢ (𝑧 = 𝑦 → (𝑤 = 𝑧 ↔ 𝑤 = 𝑦)) |
| 14 | 13 | notbid 318 |
. . . . . 6
⊢ (𝑧 = 𝑦 → (¬ 𝑤 = 𝑧 ↔ ¬ 𝑤 = 𝑦)) |
| 15 | | ax7v1 2009 |
. . . . . . . 8
⊢ (𝑥 = 𝑤 → (𝑥 = 𝑦 → 𝑤 = 𝑦)) |
| 16 | 15 | con3d 152 |
. . . . . . 7
⊢ (𝑥 = 𝑤 → (¬ 𝑤 = 𝑦 → ¬ 𝑥 = 𝑦)) |
| 17 | 16 | spimevw 1994 |
. . . . . 6
⊢ (¬
𝑤 = 𝑦 → ∃𝑥 ¬ 𝑥 = 𝑦) |
| 18 | 14, 17 | biimtrdi 253 |
. . . . 5
⊢ (𝑧 = 𝑦 → (¬ 𝑤 = 𝑧 → ∃𝑥 ¬ 𝑥 = 𝑦)) |
| 19 | | ax7v1 2009 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 → (𝑥 = 𝑦 → 𝑧 = 𝑦)) |
| 20 | 19 | con3d 152 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → (¬ 𝑧 = 𝑦 → ¬ 𝑥 = 𝑦)) |
| 21 | 20 | spimevw 1994 |
. . . . . 6
⊢ (¬
𝑧 = 𝑦 → ∃𝑥 ¬ 𝑥 = 𝑦) |
| 22 | 21 | a1d 25 |
. . . . 5
⊢ (¬
𝑧 = 𝑦 → (¬ 𝑤 = 𝑧 → ∃𝑥 ¬ 𝑥 = 𝑦)) |
| 23 | 18, 22 | pm2.61i 182 |
. . . 4
⊢ (¬
𝑤 = 𝑧 → ∃𝑥 ¬ 𝑥 = 𝑦) |
| 24 | 23 | exlimivv 1932 |
. . 3
⊢
(∃𝑤∃𝑧 ¬ 𝑤 = 𝑧 → ∃𝑥 ¬ 𝑥 = 𝑦) |
| 25 | 8, 12, 24 | mp2b 10 |
. 2
⊢
∃𝑥 ¬ 𝑥 = 𝑦 |
| 26 | | exnal 1827 |
. 2
⊢
(∃𝑥 ¬
𝑥 = 𝑦 ↔ ¬ ∀𝑥 𝑥 = 𝑦) |
| 27 | 25, 26 | mpbi 230 |
1
⊢ ¬
∀𝑥 𝑥 = 𝑦 |