Proof of Theorem sbbibOLD
Step | Hyp | Ref
| Expression |
1 | | nfs1v 2159 |
. . . . . 6
⊢
Ⅎ𝑥[𝑦 / 𝑥]𝜑 |
2 | | sbbibOLD.x |
. . . . . 6
⊢
Ⅎ𝑥𝜓 |
3 | 1, 2 | nfbi 1903 |
. . . . 5
⊢
Ⅎ𝑥([𝑦 / 𝑥]𝜑 ↔ 𝜓) |
4 | 3 | nf5ri 2194 |
. . . 4
⊢ (([𝑦 / 𝑥]𝜑 ↔ 𝜓) → ∀𝑥([𝑦 / 𝑥]𝜑 ↔ 𝜓)) |
5 | 4 | hbal 2173 |
. . 3
⊢
(∀𝑦([𝑦 / 𝑥]𝜑 ↔ 𝜓) → ∀𝑥∀𝑦([𝑦 / 𝑥]𝜑 ↔ 𝜓)) |
6 | | sbcov 2257 |
. . . . 5
⊢ ([𝑥 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝑥 / 𝑦]𝜑) |
7 | | sbbibOLD.y |
. . . . . 6
⊢
Ⅎ𝑦𝜑 |
8 | 7 | sbf 2270 |
. . . . 5
⊢ ([𝑥 / 𝑦]𝜑 ↔ 𝜑) |
9 | 6, 8 | bitri 277 |
. . . 4
⊢ ([𝑥 / 𝑦][𝑦 / 𝑥]𝜑 ↔ 𝜑) |
10 | | spsbbi 2077 |
. . . 4
⊢
(∀𝑦([𝑦 / 𝑥]𝜑 ↔ 𝜓) → ([𝑥 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝑥 / 𝑦]𝜓)) |
11 | 9, 10 | syl5bbr 287 |
. . 3
⊢
(∀𝑦([𝑦 / 𝑥]𝜑 ↔ 𝜓) → (𝜑 ↔ [𝑥 / 𝑦]𝜓)) |
12 | 5, 11 | alrimih 1823 |
. 2
⊢
(∀𝑦([𝑦 / 𝑥]𝜑 ↔ 𝜓) → ∀𝑥(𝜑 ↔ [𝑥 / 𝑦]𝜓)) |
13 | | nfs1v 2159 |
. . . . . 6
⊢
Ⅎ𝑦[𝑥 / 𝑦]𝜓 |
14 | 7, 13 | nfbi 1903 |
. . . . 5
⊢
Ⅎ𝑦(𝜑 ↔ [𝑥 / 𝑦]𝜓) |
15 | 14 | nf5ri 2194 |
. . . 4
⊢ ((𝜑 ↔ [𝑥 / 𝑦]𝜓) → ∀𝑦(𝜑 ↔ [𝑥 / 𝑦]𝜓)) |
16 | 15 | hbal 2173 |
. . 3
⊢
(∀𝑥(𝜑 ↔ [𝑥 / 𝑦]𝜓) → ∀𝑦∀𝑥(𝜑 ↔ [𝑥 / 𝑦]𝜓)) |
17 | | spsbbi 2077 |
. . . 4
⊢
(∀𝑥(𝜑 ↔ [𝑥 / 𝑦]𝜓) → ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥][𝑥 / 𝑦]𝜓)) |
18 | | sbcov 2257 |
. . . . 5
⊢ ([𝑦 / 𝑥][𝑥 / 𝑦]𝜓 ↔ [𝑦 / 𝑥]𝜓) |
19 | 2 | sbf 2270 |
. . . . 5
⊢ ([𝑦 / 𝑥]𝜓 ↔ 𝜓) |
20 | 18, 19 | bitri 277 |
. . . 4
⊢ ([𝑦 / 𝑥][𝑥 / 𝑦]𝜓 ↔ 𝜓) |
21 | 17, 20 | syl6bb 289 |
. . 3
⊢
(∀𝑥(𝜑 ↔ [𝑥 / 𝑦]𝜓) → ([𝑦 / 𝑥]𝜑 ↔ 𝜓)) |
22 | 16, 21 | alrimih 1823 |
. 2
⊢
(∀𝑥(𝜑 ↔ [𝑥 / 𝑦]𝜓) → ∀𝑦([𝑦 / 𝑥]𝜑 ↔ 𝜓)) |
23 | 12, 22 | impbii 211 |
1
⊢
(∀𝑦([𝑦 / 𝑥]𝜑 ↔ 𝜓) ↔ ∀𝑥(𝜑 ↔ [𝑥 / 𝑦]𝜓)) |