Proof of Theorem sbal2OLD
Step | Hyp | Ref
| Expression |
1 | | sbid 2257 |
. . . . 5
⊢ ([𝑦 / 𝑦]∀𝑥𝜑 ↔ ∀𝑥𝜑) |
2 | | drsb2 2267 |
. . . . 5
⊢
(∀𝑦 𝑦 = 𝑧 → ([𝑦 / 𝑦]∀𝑥𝜑 ↔ [𝑧 / 𝑦]∀𝑥𝜑)) |
3 | 1, 2 | syl5bbr 287 |
. . . 4
⊢
(∀𝑦 𝑦 = 𝑧 → (∀𝑥𝜑 ↔ [𝑧 / 𝑦]∀𝑥𝜑)) |
4 | | sbid 2257 |
. . . . . 6
⊢ ([𝑦 / 𝑦]𝜑 ↔ 𝜑) |
5 | | drsb2 2267 |
. . . . . 6
⊢
(∀𝑦 𝑦 = 𝑧 → ([𝑦 / 𝑦]𝜑 ↔ [𝑧 / 𝑦]𝜑)) |
6 | 4, 5 | syl5bbr 287 |
. . . . 5
⊢
(∀𝑦 𝑦 = 𝑧 → (𝜑 ↔ [𝑧 / 𝑦]𝜑)) |
7 | 6 | dral2 2460 |
. . . 4
⊢
(∀𝑦 𝑦 = 𝑧 → (∀𝑥𝜑 ↔ ∀𝑥[𝑧 / 𝑦]𝜑)) |
8 | 3, 7 | bitr3d 283 |
. . 3
⊢
(∀𝑦 𝑦 = 𝑧 → ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑥[𝑧 / 𝑦]𝜑)) |
9 | 8 | adantl 484 |
. 2
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ∀𝑦 𝑦 = 𝑧) → ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑥[𝑧 / 𝑦]𝜑)) |
10 | | sb4b 2499 |
. . . 4
⊢ (¬
∀𝑦 𝑦 = 𝑧 → ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑦(𝑦 = 𝑧 → ∀𝑥𝜑))) |
11 | 10 | adantl 484 |
. . 3
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑦(𝑦 = 𝑧 → ∀𝑥𝜑))) |
12 | | nfnae 2456 |
. . . . . 6
⊢
Ⅎ𝑥 ¬
∀𝑦 𝑦 = 𝑧 |
13 | | sb4b 2499 |
. . . . . 6
⊢ (¬
∀𝑦 𝑦 = 𝑧 → ([𝑧 / 𝑦]𝜑 ↔ ∀𝑦(𝑦 = 𝑧 → 𝜑))) |
14 | 12, 13 | albid 2224 |
. . . . 5
⊢ (¬
∀𝑦 𝑦 = 𝑧 → (∀𝑥[𝑧 / 𝑦]𝜑 ↔ ∀𝑥∀𝑦(𝑦 = 𝑧 → 𝜑))) |
15 | | alcom 2163 |
. . . . 5
⊢
(∀𝑥∀𝑦(𝑦 = 𝑧 → 𝜑) ↔ ∀𝑦∀𝑥(𝑦 = 𝑧 → 𝜑)) |
16 | 14, 15 | syl6bb 289 |
. . . 4
⊢ (¬
∀𝑦 𝑦 = 𝑧 → (∀𝑥[𝑧 / 𝑦]𝜑 ↔ ∀𝑦∀𝑥(𝑦 = 𝑧 → 𝜑))) |
17 | | nfnae 2456 |
. . . . 5
⊢
Ⅎ𝑦 ¬
∀𝑥 𝑥 = 𝑦 |
18 | | nfeqf1 2397 |
. . . . . 6
⊢ (¬
∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥 𝑦 = 𝑧) |
19 | | 19.21t 2206 |
. . . . . 6
⊢
(Ⅎ𝑥 𝑦 = 𝑧 → (∀𝑥(𝑦 = 𝑧 → 𝜑) ↔ (𝑦 = 𝑧 → ∀𝑥𝜑))) |
20 | 18, 19 | syl 17 |
. . . . 5
⊢ (¬
∀𝑥 𝑥 = 𝑦 → (∀𝑥(𝑦 = 𝑧 → 𝜑) ↔ (𝑦 = 𝑧 → ∀𝑥𝜑))) |
21 | 17, 20 | albid 2224 |
. . . 4
⊢ (¬
∀𝑥 𝑥 = 𝑦 → (∀𝑦∀𝑥(𝑦 = 𝑧 → 𝜑) ↔ ∀𝑦(𝑦 = 𝑧 → ∀𝑥𝜑))) |
22 | 16, 21 | sylan9bbr 513 |
. . 3
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → (∀𝑥[𝑧 / 𝑦]𝜑 ↔ ∀𝑦(𝑦 = 𝑧 → ∀𝑥𝜑))) |
23 | 11, 22 | bitr4d 284 |
. 2
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑥[𝑧 / 𝑦]𝜑)) |
24 | 9, 23 | pm2.61dan 811 |
1
⊢ (¬
∀𝑥 𝑥 = 𝑦 → ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑥[𝑧 / 𝑦]𝜑)) |