Proof of Theorem sbco3
Step | Hyp | Ref
| Expression |
1 | | drsb1 2365 |
. . 3
⊢
(∀𝑥 𝑥 = 𝑦 → ([𝑧 / 𝑥][𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑦][𝑦 / 𝑥]𝜑)) |
2 | | nfae 2304 |
. . . 4
⊢
Ⅎ𝑥∀𝑥 𝑥 = 𝑦 |
3 | | sbequ12a 2099 |
. . . . 5
⊢ (𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜑 ↔ [𝑥 / 𝑦]𝜑)) |
4 | 3 | sps 2043 |
. . . 4
⊢
(∀𝑥 𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜑 ↔ [𝑥 / 𝑦]𝜑)) |
5 | 2, 4 | sbbid 2391 |
. . 3
⊢
(∀𝑥 𝑥 = 𝑦 → ([𝑧 / 𝑥][𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑥][𝑥 / 𝑦]𝜑)) |
6 | 1, 5 | bitr3d 269 |
. 2
⊢
(∀𝑥 𝑥 = 𝑦 → ([𝑧 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑥][𝑥 / 𝑦]𝜑)) |
7 | | sbco 2400 |
. . . 4
⊢ ([𝑥 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝑥 / 𝑦]𝜑) |
8 | 7 | sbbii 1874 |
. . 3
⊢ ([𝑧 / 𝑥][𝑥 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑥][𝑥 / 𝑦]𝜑) |
9 | | nfnae 2306 |
. . . 4
⊢
Ⅎ𝑦 ¬
∀𝑥 𝑥 = 𝑦 |
10 | | nfnae 2306 |
. . . 4
⊢
Ⅎ𝑥 ¬
∀𝑥 𝑥 = 𝑦 |
11 | | nfsb2 2348 |
. . . 4
⊢ (¬
∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥[𝑦 / 𝑥]𝜑) |
12 | 9, 10, 11 | sbco2d 2404 |
. . 3
⊢ (¬
∀𝑥 𝑥 = 𝑦 → ([𝑧 / 𝑥][𝑥 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑦][𝑦 / 𝑥]𝜑)) |
13 | 8, 12 | syl5rbbr 274 |
. 2
⊢ (¬
∀𝑥 𝑥 = 𝑦 → ([𝑧 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑥][𝑥 / 𝑦]𝜑)) |
14 | 6, 13 | pm2.61i 175 |
1
⊢ ([𝑧 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑥][𝑥 / 𝑦]𝜑) |