Proof of Theorem wl-exeq
Step | Hyp | Ref
| Expression |
1 | | nfeqf 2381 |
. . . . . . . . 9
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥 𝑦 = 𝑧) |
2 | 1 | 19.9d 2202 |
. . . . . . . 8
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → (∃𝑥 𝑦 = 𝑧 → 𝑦 = 𝑧)) |
3 | 2 | impancom 455 |
. . . . . . 7
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ∃𝑥 𝑦 = 𝑧) → (¬ ∀𝑥 𝑥 = 𝑧 → 𝑦 = 𝑧)) |
4 | 3 | orrd 863 |
. . . . . 6
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ∃𝑥 𝑦 = 𝑧) → (∀𝑥 𝑥 = 𝑧 ∨ 𝑦 = 𝑧)) |
5 | 4 | expcom 417 |
. . . . 5
⊢
(∃𝑥 𝑦 = 𝑧 → (¬ ∀𝑥 𝑥 = 𝑦 → (∀𝑥 𝑥 = 𝑧 ∨ 𝑦 = 𝑧))) |
6 | 5 | orrd 863 |
. . . 4
⊢
(∃𝑥 𝑦 = 𝑧 → (∀𝑥 𝑥 = 𝑦 ∨ (∀𝑥 𝑥 = 𝑧 ∨ 𝑦 = 𝑧))) |
7 | | 3orass 1092 |
. . . 4
⊢
((∀𝑥 𝑥 = 𝑦 ∨ ∀𝑥 𝑥 = 𝑧 ∨ 𝑦 = 𝑧) ↔ (∀𝑥 𝑥 = 𝑦 ∨ (∀𝑥 𝑥 = 𝑧 ∨ 𝑦 = 𝑧))) |
8 | 6, 7 | sylibr 237 |
. . 3
⊢
(∃𝑥 𝑦 = 𝑧 → (∀𝑥 𝑥 = 𝑦 ∨ ∀𝑥 𝑥 = 𝑧 ∨ 𝑦 = 𝑧)) |
9 | | 3orrot 1094 |
. . 3
⊢ ((𝑦 = 𝑧 ∨ ∀𝑥 𝑥 = 𝑦 ∨ ∀𝑥 𝑥 = 𝑧) ↔ (∀𝑥 𝑥 = 𝑦 ∨ ∀𝑥 𝑥 = 𝑧 ∨ 𝑦 = 𝑧)) |
10 | 8, 9 | sylibr 237 |
. 2
⊢
(∃𝑥 𝑦 = 𝑧 → (𝑦 = 𝑧 ∨ ∀𝑥 𝑥 = 𝑦 ∨ ∀𝑥 𝑥 = 𝑧)) |
11 | | 19.8a 2179 |
. . 3
⊢ (𝑦 = 𝑧 → ∃𝑥 𝑦 = 𝑧) |
12 | | ax6e 2383 |
. . . . 5
⊢
∃𝑥 𝑥 = 𝑧 |
13 | | ax7 2024 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧)) |
14 | 13 | com12 32 |
. . . . 5
⊢ (𝑥 = 𝑧 → (𝑥 = 𝑦 → 𝑦 = 𝑧)) |
15 | 12, 14 | eximii 1844 |
. . . 4
⊢
∃𝑥(𝑥 = 𝑦 → 𝑦 = 𝑧) |
16 | 15 | 19.35i 1886 |
. . 3
⊢
(∀𝑥 𝑥 = 𝑦 → ∃𝑥 𝑦 = 𝑧) |
17 | | ax6e 2383 |
. . . . 5
⊢
∃𝑥 𝑥 = 𝑦 |
18 | 17, 13 | eximii 1844 |
. . . 4
⊢
∃𝑥(𝑥 = 𝑧 → 𝑦 = 𝑧) |
19 | 18 | 19.35i 1886 |
. . 3
⊢
(∀𝑥 𝑥 = 𝑧 → ∃𝑥 𝑦 = 𝑧) |
20 | 11, 16, 19 | 3jaoi 1429 |
. 2
⊢ ((𝑦 = 𝑧 ∨ ∀𝑥 𝑥 = 𝑦 ∨ ∀𝑥 𝑥 = 𝑧) → ∃𝑥 𝑦 = 𝑧) |
21 | 10, 20 | impbii 212 |
1
⊢
(∃𝑥 𝑦 = 𝑧 ↔ (𝑦 = 𝑧 ∨ ∀𝑥 𝑥 = 𝑦 ∨ ∀𝑥 𝑥 = 𝑧)) |