Proof of Theorem sbal2
Step | Hyp | Ref
| Expression |
1 | | sb4b 2358 |
. . . . 5
⊢ (¬
∀𝑦 𝑦 = 𝑧 → ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑦(𝑦 = 𝑧 → ∀𝑥𝜑))) |
2 | 1 | adantl 482 |
. . . 4
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑦(𝑦 = 𝑧 → ∀𝑥𝜑))) |
3 | | nfnae 2318 |
. . . . . 6
⊢
Ⅎ𝑥 ¬
∀𝑦 𝑦 = 𝑧 |
4 | | sb4b 2358 |
. . . . . 6
⊢ (¬
∀𝑦 𝑦 = 𝑧 → ([𝑧 / 𝑦]𝜑 ↔ ∀𝑦(𝑦 = 𝑧 → 𝜑))) |
5 | 3, 4 | albid 2090 |
. . . . 5
⊢ (¬
∀𝑦 𝑦 = 𝑧 → (∀𝑥[𝑧 / 𝑦]𝜑 ↔ ∀𝑥∀𝑦(𝑦 = 𝑧 → 𝜑))) |
6 | | alcom 2037 |
. . . . . 6
⊢
(∀𝑥∀𝑦(𝑦 = 𝑧 → 𝜑) ↔ ∀𝑦∀𝑥(𝑦 = 𝑧 → 𝜑)) |
7 | | nfnae 2318 |
. . . . . . 7
⊢
Ⅎ𝑦 ¬
∀𝑥 𝑥 = 𝑦 |
8 | | nfeqf1 2299 |
. . . . . . . 8
⊢ (¬
∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥 𝑦 = 𝑧) |
9 | | 19.21t 2073 |
. . . . . . . 8
⊢
(Ⅎ𝑥 𝑦 = 𝑧 → (∀𝑥(𝑦 = 𝑧 → 𝜑) ↔ (𝑦 = 𝑧 → ∀𝑥𝜑))) |
10 | 8, 9 | syl 17 |
. . . . . . 7
⊢ (¬
∀𝑥 𝑥 = 𝑦 → (∀𝑥(𝑦 = 𝑧 → 𝜑) ↔ (𝑦 = 𝑧 → ∀𝑥𝜑))) |
11 | 7, 10 | albid 2090 |
. . . . . 6
⊢ (¬
∀𝑥 𝑥 = 𝑦 → (∀𝑦∀𝑥(𝑦 = 𝑧 → 𝜑) ↔ ∀𝑦(𝑦 = 𝑧 → ∀𝑥𝜑))) |
12 | 6, 11 | syl5bb 272 |
. . . . 5
⊢ (¬
∀𝑥 𝑥 = 𝑦 → (∀𝑥∀𝑦(𝑦 = 𝑧 → 𝜑) ↔ ∀𝑦(𝑦 = 𝑧 → ∀𝑥𝜑))) |
13 | 5, 12 | sylan9bbr 737 |
. . . 4
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → (∀𝑥[𝑧 / 𝑦]𝜑 ↔ ∀𝑦(𝑦 = 𝑧 → ∀𝑥𝜑))) |
14 | 2, 13 | bitr4d 271 |
. . 3
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑥[𝑧 / 𝑦]𝜑)) |
15 | 14 | ex 450 |
. 2
⊢ (¬
∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑦 𝑦 = 𝑧 → ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑥[𝑧 / 𝑦]𝜑))) |
16 | | sbid 2114 |
. . . 4
⊢ ([𝑦 / 𝑦]∀𝑥𝜑 ↔ ∀𝑥𝜑) |
17 | | drsb2 2378 |
. . . 4
⊢
(∀𝑦 𝑦 = 𝑧 → ([𝑦 / 𝑦]∀𝑥𝜑 ↔ [𝑧 / 𝑦]∀𝑥𝜑)) |
18 | 16, 17 | syl5bbr 274 |
. . 3
⊢
(∀𝑦 𝑦 = 𝑧 → (∀𝑥𝜑 ↔ [𝑧 / 𝑦]∀𝑥𝜑)) |
19 | | sbid 2114 |
. . . . 5
⊢ ([𝑦 / 𝑦]𝜑 ↔ 𝜑) |
20 | | drsb2 2378 |
. . . . 5
⊢
(∀𝑦 𝑦 = 𝑧 → ([𝑦 / 𝑦]𝜑 ↔ [𝑧 / 𝑦]𝜑)) |
21 | 19, 20 | syl5bbr 274 |
. . . 4
⊢
(∀𝑦 𝑦 = 𝑧 → (𝜑 ↔ [𝑧 / 𝑦]𝜑)) |
22 | 21 | dral2 2324 |
. . 3
⊢
(∀𝑦 𝑦 = 𝑧 → (∀𝑥𝜑 ↔ ∀𝑥[𝑧 / 𝑦]𝜑)) |
23 | 18, 22 | bitr3d 270 |
. 2
⊢
(∀𝑦 𝑦 = 𝑧 → ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑥[𝑧 / 𝑦]𝜑)) |
24 | 15, 23 | pm2.61d2 172 |
1
⊢ (¬
∀𝑥 𝑥 = 𝑦 → ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑥[𝑧 / 𝑦]𝜑)) |