Proof of Theorem sbco3
Step | Hyp | Ref
| Expression |
1 | | drsb1 2524 |
. . 3
⊢
(∀𝑥 𝑥 = 𝑦 → ([𝑧 / 𝑥][𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑦][𝑦 / 𝑥]𝜑)) |
2 | | nfae 2468 |
. . . 4
⊢
Ⅎ𝑥∀𝑥 𝑥 = 𝑦 |
3 | | sbequ12a 2269 |
. . . . 5
⊢ (𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜑 ↔ [𝑥 / 𝑦]𝜑)) |
4 | 3 | sps 2209 |
. . . 4
⊢
(∀𝑥 𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜑 ↔ [𝑥 / 𝑦]𝜑)) |
5 | 2, 4 | sbbid 2550 |
. . 3
⊢
(∀𝑥 𝑥 = 𝑦 → ([𝑧 / 𝑥][𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑥][𝑥 / 𝑦]𝜑)) |
6 | 1, 5 | bitr3d 270 |
. 2
⊢
(∀𝑥 𝑥 = 𝑦 → ([𝑧 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑥][𝑥 / 𝑦]𝜑)) |
7 | | sbco 2559 |
. . . 4
⊢ ([𝑥 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝑥 / 𝑦]𝜑) |
8 | 7 | sbbii 2056 |
. . 3
⊢ ([𝑧 / 𝑥][𝑥 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑥][𝑥 / 𝑦]𝜑) |
9 | | nfnae 2470 |
. . . 4
⊢
Ⅎ𝑦 ¬
∀𝑥 𝑥 = 𝑦 |
10 | | nfnae 2470 |
. . . 4
⊢
Ⅎ𝑥 ¬
∀𝑥 𝑥 = 𝑦 |
11 | | nfsb2 2507 |
. . . 4
⊢ (¬
∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥[𝑦 / 𝑥]𝜑) |
12 | 9, 10, 11 | sbco2d 2563 |
. . 3
⊢ (¬
∀𝑥 𝑥 = 𝑦 → ([𝑧 / 𝑥][𝑥 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑦][𝑦 / 𝑥]𝜑)) |
13 | 8, 12 | syl5rbbr 275 |
. 2
⊢ (¬
∀𝑥 𝑥 = 𝑦 → ([𝑧 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑥][𝑥 / 𝑦]𝜑)) |
14 | 6, 13 | pm2.61i 176 |
1
⊢ ([𝑧 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑥][𝑥 / 𝑦]𝜑) |