Proof of Theorem dfich2ai
Step | Hyp | Ref
| Expression |
1 | | sbco4 2284 |
. . . . 5
⊢ ([𝑦 / 𝑎][𝑥 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑥 / 𝑧][𝑦 / 𝑥][𝑧 / 𝑦]𝜑) |
2 | 1 | bicomi 226 |
. . . 4
⊢ ([𝑥 / 𝑧][𝑦 / 𝑥][𝑧 / 𝑦]𝜑 ↔ [𝑦 / 𝑎][𝑥 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜑) |
3 | 2 | bibi1i 341 |
. . 3
⊢ (([𝑥 / 𝑧][𝑦 / 𝑥][𝑧 / 𝑦]𝜑 ↔ 𝜑) ↔ ([𝑦 / 𝑎][𝑥 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ 𝜑)) |
4 | 3 | 2albii 1821 |
. 2
⊢
(∀𝑥∀𝑦([𝑥 / 𝑧][𝑦 / 𝑥][𝑧 / 𝑦]𝜑 ↔ 𝜑) ↔ ∀𝑥∀𝑦([𝑦 / 𝑎][𝑥 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ 𝜑)) |
5 | | nfs1v 2160 |
. . . . . . 7
⊢
Ⅎ𝑦[𝑏 / 𝑦]𝜑 |
6 | 5 | nfsbv 2349 |
. . . . . 6
⊢
Ⅎ𝑦[𝑎 / 𝑥][𝑏 / 𝑦]𝜑 |
7 | 6 | nfsbv 2349 |
. . . . 5
⊢
Ⅎ𝑦[𝑥 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜑 |
8 | | nfv 1915 |
. . . . 5
⊢
Ⅎ𝑎𝜑 |
9 | 7, 8 | sbbib 2380 |
. . . 4
⊢
(∀𝑦([𝑦 / 𝑎][𝑥 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ 𝜑) ↔ ∀𝑎([𝑥 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑎 / 𝑦]𝜑)) |
10 | 9 | albii 1820 |
. . 3
⊢
(∀𝑥∀𝑦([𝑦 / 𝑎][𝑥 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ 𝜑) ↔ ∀𝑥∀𝑎([𝑥 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑎 / 𝑦]𝜑)) |
11 | | alcom 2163 |
. . . . 5
⊢
(∀𝑥∀𝑎([𝑥 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑎 / 𝑦]𝜑) ↔ ∀𝑎∀𝑥([𝑥 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑎 / 𝑦]𝜑)) |
12 | | nfs1v 2160 |
. . . . . . 7
⊢
Ⅎ𝑥[𝑎 / 𝑥][𝑏 / 𝑦]𝜑 |
13 | | nfv 1915 |
. . . . . . 7
⊢
Ⅎ𝑏[𝑎 / 𝑦]𝜑 |
14 | 12, 13 | sbbib 2380 |
. . . . . 6
⊢
(∀𝑥([𝑥 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑎 / 𝑦]𝜑) ↔ ∀𝑏([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑏 / 𝑥][𝑎 / 𝑦]𝜑)) |
15 | 14 | albii 1820 |
. . . . 5
⊢
(∀𝑎∀𝑥([𝑥 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑎 / 𝑦]𝜑) ↔ ∀𝑎∀𝑏([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑏 / 𝑥][𝑎 / 𝑦]𝜑)) |
16 | 11, 15 | bitri 277 |
. . . 4
⊢
(∀𝑥∀𝑎([𝑥 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑎 / 𝑦]𝜑) ↔ ∀𝑎∀𝑏([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑏 / 𝑥][𝑎 / 𝑦]𝜑)) |
17 | | 2sp 2185 |
. . . 4
⊢
(∀𝑎∀𝑏([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑏 / 𝑥][𝑎 / 𝑦]𝜑) → ([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑏 / 𝑥][𝑎 / 𝑦]𝜑)) |
18 | 16, 17 | sylbi 219 |
. . 3
⊢
(∀𝑥∀𝑎([𝑥 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑎 / 𝑦]𝜑) → ([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑏 / 𝑥][𝑎 / 𝑦]𝜑)) |
19 | 10, 18 | sylbi 219 |
. 2
⊢
(∀𝑥∀𝑦([𝑦 / 𝑎][𝑥 / 𝑏][𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ 𝜑) → ([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑏 / 𝑥][𝑎 / 𝑦]𝜑)) |
20 | 4, 19 | sylbi 219 |
1
⊢
(∀𝑥∀𝑦([𝑥 / 𝑧][𝑦 / 𝑥][𝑧 / 𝑦]𝜑 ↔ 𝜑) → ([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑏 / 𝑥][𝑎 / 𝑦]𝜑)) |