Proof of Theorem sbco3
Step | Hyp | Ref
| Expression |
1 | | drsb1 2531 |
. . 3
⊢
(∀𝑥 𝑥 = 𝑦 → ([𝑧 / 𝑥][𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑦][𝑦 / 𝑥]𝜑)) |
2 | | nfae 2450 |
. . . 4
⊢
Ⅎ𝑥∀𝑥 𝑥 = 𝑦 |
3 | | sbequ12a 2247 |
. . . . 5
⊢ (𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜑 ↔ [𝑥 / 𝑦]𝜑)) |
4 | 3 | sps 2174 |
. . . 4
⊢
(∀𝑥 𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜑 ↔ [𝑥 / 𝑦]𝜑)) |
5 | 2, 4 | sbbid 2237 |
. . 3
⊢
(∀𝑥 𝑥 = 𝑦 → ([𝑧 / 𝑥][𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑥][𝑥 / 𝑦]𝜑)) |
6 | 1, 5 | bitr3d 282 |
. 2
⊢
(∀𝑥 𝑥 = 𝑦 → ([𝑧 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑥][𝑥 / 𝑦]𝜑)) |
7 | | sbco 2545 |
. . . 4
⊢ ([𝑥 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝑥 / 𝑦]𝜑) |
8 | 7 | sbbii 2072 |
. . 3
⊢ ([𝑧 / 𝑥][𝑥 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑥][𝑥 / 𝑦]𝜑) |
9 | | nfnae 2451 |
. . . 4
⊢
Ⅎ𝑦 ¬
∀𝑥 𝑥 = 𝑦 |
10 | | nfnae 2451 |
. . . 4
⊢
Ⅎ𝑥 ¬
∀𝑥 𝑥 = 𝑦 |
11 | | nfsb2 2518 |
. . . 4
⊢ (¬
∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥[𝑦 / 𝑥]𝜑) |
12 | 9, 10, 11 | sbco2d 2550 |
. . 3
⊢ (¬
∀𝑥 𝑥 = 𝑦 → ([𝑧 / 𝑥][𝑥 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑦][𝑦 / 𝑥]𝜑)) |
13 | 8, 12 | syl5rbbr 287 |
. 2
⊢ (¬
∀𝑥 𝑥 = 𝑦 → ([𝑧 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑥][𝑥 / 𝑦]𝜑)) |
14 | 6, 13 | pm2.61i 183 |
1
⊢ ([𝑧 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑥][𝑥 / 𝑦]𝜑) |