Step | Hyp | Ref
| Expression |
1 | | el 5398 |
. . . 4
⊢
∃𝑤 𝑥 ∈ 𝑤 |
2 | | ax-nul 5267 |
. . . . 5
⊢
∃𝑧∀𝑥 ¬ 𝑥 ∈ 𝑧 |
3 | | elequ1 2114 |
. . . . . . 7
⊢ (𝑥 = 𝑤 → (𝑥 ∈ 𝑧 ↔ 𝑤 ∈ 𝑧)) |
4 | 3 | notbid 318 |
. . . . . 6
⊢ (𝑥 = 𝑤 → (¬ 𝑥 ∈ 𝑧 ↔ ¬ 𝑤 ∈ 𝑧)) |
5 | 4 | spw 2038 |
. . . . 5
⊢
(∀𝑥 ¬
𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑧) |
6 | 2, 5 | eximii 1840 |
. . . 4
⊢
∃𝑧 ¬ 𝑥 ∈ 𝑧 |
7 | | exdistrv 1960 |
. . . 4
⊢
(∃𝑤∃𝑧(𝑥 ∈ 𝑤 ∧ ¬ 𝑥 ∈ 𝑧) ↔ (∃𝑤 𝑥 ∈ 𝑤 ∧ ∃𝑧 ¬ 𝑥 ∈ 𝑧)) |
8 | 1, 6, 7 | mpbir2an 710 |
. . 3
⊢
∃𝑤∃𝑧(𝑥 ∈ 𝑤 ∧ ¬ 𝑥 ∈ 𝑧) |
9 | | ax9v2 2120 |
. . . . . 6
⊢ (𝑤 = 𝑧 → (𝑥 ∈ 𝑤 → 𝑥 ∈ 𝑧)) |
10 | 9 | com12 32 |
. . . . 5
⊢ (𝑥 ∈ 𝑤 → (𝑤 = 𝑧 → 𝑥 ∈ 𝑧)) |
11 | 10 | con3dimp 410 |
. . . 4
⊢ ((𝑥 ∈ 𝑤 ∧ ¬ 𝑥 ∈ 𝑧) → ¬ 𝑤 = 𝑧) |
12 | 11 | 2eximi 1839 |
. . 3
⊢
(∃𝑤∃𝑧(𝑥 ∈ 𝑤 ∧ ¬ 𝑥 ∈ 𝑧) → ∃𝑤∃𝑧 ¬ 𝑤 = 𝑧) |
13 | | equequ2 2030 |
. . . . . . 7
⊢ (𝑧 = 𝑦 → (𝑤 = 𝑧 ↔ 𝑤 = 𝑦)) |
14 | 13 | notbid 318 |
. . . . . 6
⊢ (𝑧 = 𝑦 → (¬ 𝑤 = 𝑧 ↔ ¬ 𝑤 = 𝑦)) |
15 | | ax7v1 2014 |
. . . . . . . 8
⊢ (𝑥 = 𝑤 → (𝑥 = 𝑦 → 𝑤 = 𝑦)) |
16 | 15 | con3d 152 |
. . . . . . 7
⊢ (𝑥 = 𝑤 → (¬ 𝑤 = 𝑦 → ¬ 𝑥 = 𝑦)) |
17 | 16 | spimevw 1999 |
. . . . . 6
⊢ (¬
𝑤 = 𝑦 → ∃𝑥 ¬ 𝑥 = 𝑦) |
18 | 14, 17 | syl6bi 253 |
. . . . 5
⊢ (𝑧 = 𝑦 → (¬ 𝑤 = 𝑧 → ∃𝑥 ¬ 𝑥 = 𝑦)) |
19 | | ax7v1 2014 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 → (𝑥 = 𝑦 → 𝑧 = 𝑦)) |
20 | 19 | con3d 152 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → (¬ 𝑧 = 𝑦 → ¬ 𝑥 = 𝑦)) |
21 | 20 | spimevw 1999 |
. . . . . 6
⊢ (¬
𝑧 = 𝑦 → ∃𝑥 ¬ 𝑥 = 𝑦) |
22 | 21 | a1d 25 |
. . . . 5
⊢ (¬
𝑧 = 𝑦 → (¬ 𝑤 = 𝑧 → ∃𝑥 ¬ 𝑥 = 𝑦)) |
23 | 18, 22 | pm2.61i 182 |
. . . 4
⊢ (¬
𝑤 = 𝑧 → ∃𝑥 ¬ 𝑥 = 𝑦) |
24 | 23 | exlimivv 1936 |
. . 3
⊢
(∃𝑤∃𝑧 ¬ 𝑤 = 𝑧 → ∃𝑥 ¬ 𝑥 = 𝑦) |
25 | 8, 12, 24 | mp2b 10 |
. 2
⊢
∃𝑥 ¬ 𝑥 = 𝑦 |
26 | | exnal 1830 |
. 2
⊢
(∃𝑥 ¬
𝑥 = 𝑦 ↔ ¬ ∀𝑥 𝑥 = 𝑦) |
27 | 25, 26 | mpbi 229 |
1
⊢ ¬
∀𝑥 𝑥 = 𝑦 |