Step | Hyp | Ref
| Expression |
1 | | elALT2 5292 |
. . . 4
⊢
∃𝑤 𝑥 ∈ 𝑤 |
2 | | ax-nul 5230 |
. . . . 5
⊢
∃𝑧∀𝑥 ¬ 𝑥 ∈ 𝑧 |
3 | | elequ1 2113 |
. . . . . . 7
⊢ (𝑥 = 𝑤 → (𝑥 ∈ 𝑧 ↔ 𝑤 ∈ 𝑧)) |
4 | 3 | notbid 318 |
. . . . . 6
⊢ (𝑥 = 𝑤 → (¬ 𝑥 ∈ 𝑧 ↔ ¬ 𝑤 ∈ 𝑧)) |
5 | 4 | spw 2037 |
. . . . 5
⊢
(∀𝑥 ¬
𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑧) |
6 | 2, 5 | eximii 1839 |
. . . 4
⊢
∃𝑧 ¬ 𝑥 ∈ 𝑧 |
7 | | exdistrv 1959 |
. . . 4
⊢
(∃𝑤∃𝑧(𝑥 ∈ 𝑤 ∧ ¬ 𝑥 ∈ 𝑧) ↔ (∃𝑤 𝑥 ∈ 𝑤 ∧ ∃𝑧 ¬ 𝑥 ∈ 𝑧)) |
8 | 1, 6, 7 | mpbir2an 708 |
. . 3
⊢
∃𝑤∃𝑧(𝑥 ∈ 𝑤 ∧ ¬ 𝑥 ∈ 𝑧) |
9 | | ax9v2 2119 |
. . . . . 6
⊢ (𝑤 = 𝑧 → (𝑥 ∈ 𝑤 → 𝑥 ∈ 𝑧)) |
10 | 9 | com12 32 |
. . . . 5
⊢ (𝑥 ∈ 𝑤 → (𝑤 = 𝑧 → 𝑥 ∈ 𝑧)) |
11 | 10 | con3dimp 409 |
. . . 4
⊢ ((𝑥 ∈ 𝑤 ∧ ¬ 𝑥 ∈ 𝑧) → ¬ 𝑤 = 𝑧) |
12 | 11 | 2eximi 1838 |
. . 3
⊢
(∃𝑤∃𝑧(𝑥 ∈ 𝑤 ∧ ¬ 𝑥 ∈ 𝑧) → ∃𝑤∃𝑧 ¬ 𝑤 = 𝑧) |
13 | | equequ2 2029 |
. . . . . . 7
⊢ (𝑧 = 𝑦 → (𝑤 = 𝑧 ↔ 𝑤 = 𝑦)) |
14 | 13 | notbid 318 |
. . . . . 6
⊢ (𝑧 = 𝑦 → (¬ 𝑤 = 𝑧 ↔ ¬ 𝑤 = 𝑦)) |
15 | | ax7v1 2013 |
. . . . . . . 8
⊢ (𝑥 = 𝑤 → (𝑥 = 𝑦 → 𝑤 = 𝑦)) |
16 | 15 | con3d 152 |
. . . . . . 7
⊢ (𝑥 = 𝑤 → (¬ 𝑤 = 𝑦 → ¬ 𝑥 = 𝑦)) |
17 | 16 | spimevw 1998 |
. . . . . 6
⊢ (¬
𝑤 = 𝑦 → ∃𝑥 ¬ 𝑥 = 𝑦) |
18 | 14, 17 | syl6bi 252 |
. . . . 5
⊢ (𝑧 = 𝑦 → (¬ 𝑤 = 𝑧 → ∃𝑥 ¬ 𝑥 = 𝑦)) |
19 | | ax7v1 2013 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 → (𝑥 = 𝑦 → 𝑧 = 𝑦)) |
20 | 19 | con3d 152 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → (¬ 𝑧 = 𝑦 → ¬ 𝑥 = 𝑦)) |
21 | 20 | spimevw 1998 |
. . . . . 6
⊢ (¬
𝑧 = 𝑦 → ∃𝑥 ¬ 𝑥 = 𝑦) |
22 | 21 | a1d 25 |
. . . . 5
⊢ (¬
𝑧 = 𝑦 → (¬ 𝑤 = 𝑧 → ∃𝑥 ¬ 𝑥 = 𝑦)) |
23 | 18, 22 | pm2.61i 182 |
. . . 4
⊢ (¬
𝑤 = 𝑧 → ∃𝑥 ¬ 𝑥 = 𝑦) |
24 | 23 | exlimivv 1935 |
. . 3
⊢
(∃𝑤∃𝑧 ¬ 𝑤 = 𝑧 → ∃𝑥 ¬ 𝑥 = 𝑦) |
25 | 8, 12, 24 | mp2b 10 |
. 2
⊢
∃𝑥 ¬ 𝑥 = 𝑦 |
26 | | exnal 1829 |
. 2
⊢
(∃𝑥 ¬
𝑥 = 𝑦 ↔ ¬ ∀𝑥 𝑥 = 𝑦) |
27 | 25, 26 | mpbi 229 |
1
⊢ ¬
∀𝑥 𝑥 = 𝑦 |