Proof of Theorem sbal1
Step | Hyp | Ref
| Expression |
1 | | sb4b 2474 |
. . . . 5
⊢ (¬
∀𝑦 𝑦 = 𝑧 → ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑦(𝑦 = 𝑧 → ∀𝑥𝜑))) |
2 | | nfnae 2433 |
. . . . . 6
⊢
Ⅎ𝑦 ¬
∀𝑥 𝑥 = 𝑧 |
3 | | nfeqf2 2376 |
. . . . . . 7
⊢ (¬
∀𝑥 𝑥 = 𝑧 → Ⅎ𝑥 𝑦 = 𝑧) |
4 | | 19.21t 2204 |
. . . . . . . 8
⊢
(Ⅎ𝑥 𝑦 = 𝑧 → (∀𝑥(𝑦 = 𝑧 → 𝜑) ↔ (𝑦 = 𝑧 → ∀𝑥𝜑))) |
5 | 4 | bicomd 226 |
. . . . . . 7
⊢
(Ⅎ𝑥 𝑦 = 𝑧 → ((𝑦 = 𝑧 → ∀𝑥𝜑) ↔ ∀𝑥(𝑦 = 𝑧 → 𝜑))) |
6 | 3, 5 | syl 17 |
. . . . . 6
⊢ (¬
∀𝑥 𝑥 = 𝑧 → ((𝑦 = 𝑧 → ∀𝑥𝜑) ↔ ∀𝑥(𝑦 = 𝑧 → 𝜑))) |
7 | 2, 6 | albid 2220 |
. . . . 5
⊢ (¬
∀𝑥 𝑥 = 𝑧 → (∀𝑦(𝑦 = 𝑧 → ∀𝑥𝜑) ↔ ∀𝑦∀𝑥(𝑦 = 𝑧 → 𝜑))) |
8 | 1, 7 | sylan9bbr 514 |
. . . 4
⊢ ((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑦∀𝑥(𝑦 = 𝑧 → 𝜑))) |
9 | | nfnae 2433 |
. . . . . . 7
⊢
Ⅎ𝑥 ¬
∀𝑦 𝑦 = 𝑧 |
10 | | sb4b 2474 |
. . . . . . 7
⊢ (¬
∀𝑦 𝑦 = 𝑧 → ([𝑧 / 𝑦]𝜑 ↔ ∀𝑦(𝑦 = 𝑧 → 𝜑))) |
11 | 9, 10 | albid 2220 |
. . . . . 6
⊢ (¬
∀𝑦 𝑦 = 𝑧 → (∀𝑥[𝑧 / 𝑦]𝜑 ↔ ∀𝑥∀𝑦(𝑦 = 𝑧 → 𝜑))) |
12 | | alcom 2160 |
. . . . . 6
⊢
(∀𝑥∀𝑦(𝑦 = 𝑧 → 𝜑) ↔ ∀𝑦∀𝑥(𝑦 = 𝑧 → 𝜑)) |
13 | 11, 12 | bitrdi 290 |
. . . . 5
⊢ (¬
∀𝑦 𝑦 = 𝑧 → (∀𝑥[𝑧 / 𝑦]𝜑 ↔ ∀𝑦∀𝑥(𝑦 = 𝑧 → 𝜑))) |
14 | 13 | adantl 485 |
. . . 4
⊢ ((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → (∀𝑥[𝑧 / 𝑦]𝜑 ↔ ∀𝑦∀𝑥(𝑦 = 𝑧 → 𝜑))) |
15 | 8, 14 | bitr4d 285 |
. . 3
⊢ ((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑥[𝑧 / 𝑦]𝜑)) |
16 | 15 | ex 416 |
. 2
⊢ (¬
∀𝑥 𝑥 = 𝑧 → (¬ ∀𝑦 𝑦 = 𝑧 → ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑥[𝑧 / 𝑦]𝜑))) |
17 | | sbequ12 2249 |
. . . 4
⊢ (𝑦 = 𝑧 → (∀𝑥𝜑 ↔ [𝑧 / 𝑦]∀𝑥𝜑)) |
18 | 17 | sps 2182 |
. . 3
⊢
(∀𝑦 𝑦 = 𝑧 → (∀𝑥𝜑 ↔ [𝑧 / 𝑦]∀𝑥𝜑)) |
19 | | sbequ12 2249 |
. . . . 5
⊢ (𝑦 = 𝑧 → (𝜑 ↔ [𝑧 / 𝑦]𝜑)) |
20 | 19 | sps 2182 |
. . . 4
⊢
(∀𝑦 𝑦 = 𝑧 → (𝜑 ↔ [𝑧 / 𝑦]𝜑)) |
21 | 20 | dral2 2437 |
. . 3
⊢
(∀𝑦 𝑦 = 𝑧 → (∀𝑥𝜑 ↔ ∀𝑥[𝑧 / 𝑦]𝜑)) |
22 | 18, 21 | bitr3d 284 |
. 2
⊢
(∀𝑦 𝑦 = 𝑧 → ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑥[𝑧 / 𝑦]𝜑)) |
23 | 16, 22 | pm2.61d2 184 |
1
⊢ (¬
∀𝑥 𝑥 = 𝑧 → ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑥[𝑧 / 𝑦]𝜑)) |