Step | Hyp | Ref
| Expression |
1 | | mo23.1 |
. . . . 5
⊢
Ⅎ𝑦𝜑 |
2 | | nfv 1461 |
. . . . 5
⊢
Ⅎ𝑦 𝑥 = 𝑧 |
3 | 1, 2 | nfim 1504 |
. . . 4
⊢
Ⅎ𝑦(𝜑 → 𝑥 = 𝑧) |
4 | 3 | nfal 1508 |
. . 3
⊢
Ⅎ𝑦∀𝑥(𝜑 → 𝑥 = 𝑧) |
5 | | nfv 1461 |
. . 3
⊢
Ⅎ𝑧∀𝑥(𝜑 → 𝑥 = 𝑦) |
6 | | equequ2 1639 |
. . . . 5
⊢ (𝑧 = 𝑦 → (𝑥 = 𝑧 ↔ 𝑥 = 𝑦)) |
7 | 6 | imbi2d 228 |
. . . 4
⊢ (𝑧 = 𝑦 → ((𝜑 → 𝑥 = 𝑧) ↔ (𝜑 → 𝑥 = 𝑦))) |
8 | 7 | albidv 1745 |
. . 3
⊢ (𝑧 = 𝑦 → (∀𝑥(𝜑 → 𝑥 = 𝑧) ↔ ∀𝑥(𝜑 → 𝑥 = 𝑦))) |
9 | 4, 5, 8 | cbvex 1679 |
. 2
⊢
(∃𝑧∀𝑥(𝜑 → 𝑥 = 𝑧) ↔ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦)) |
10 | | nfs1v 1856 |
. . . . . . . 8
⊢
Ⅎ𝑥[𝑦 / 𝑥]𝜑 |
11 | | nfv 1461 |
. . . . . . . 8
⊢
Ⅎ𝑥 𝑦 = 𝑧 |
12 | 10, 11 | nfim 1504 |
. . . . . . 7
⊢
Ⅎ𝑥([𝑦 / 𝑥]𝜑 → 𝑦 = 𝑧) |
13 | | sbequ2 1692 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜑 → 𝜑)) |
14 | | ax-8 1435 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧)) |
15 | 13, 14 | imim12d 73 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → ((𝜑 → 𝑥 = 𝑧) → ([𝑦 / 𝑥]𝜑 → 𝑦 = 𝑧))) |
16 | 3, 12, 15 | cbv3 1670 |
. . . . . 6
⊢
(∀𝑥(𝜑 → 𝑥 = 𝑧) → ∀𝑦([𝑦 / 𝑥]𝜑 → 𝑦 = 𝑧)) |
17 | 16 | ancli 316 |
. . . . 5
⊢
(∀𝑥(𝜑 → 𝑥 = 𝑧) → (∀𝑥(𝜑 → 𝑥 = 𝑧) ∧ ∀𝑦([𝑦 / 𝑥]𝜑 → 𝑦 = 𝑧))) |
18 | 3 | nfri 1452 |
. . . . . 6
⊢ ((𝜑 → 𝑥 = 𝑧) → ∀𝑦(𝜑 → 𝑥 = 𝑧)) |
19 | 12 | nfri 1452 |
. . . . . 6
⊢ (([𝑦 / 𝑥]𝜑 → 𝑦 = 𝑧) → ∀𝑥([𝑦 / 𝑥]𝜑 → 𝑦 = 𝑧)) |
20 | 18, 19 | aaanh 1518 |
. . . . 5
⊢
(∀𝑥∀𝑦((𝜑 → 𝑥 = 𝑧) ∧ ([𝑦 / 𝑥]𝜑 → 𝑦 = 𝑧)) ↔ (∀𝑥(𝜑 → 𝑥 = 𝑧) ∧ ∀𝑦([𝑦 / 𝑥]𝜑 → 𝑦 = 𝑧))) |
21 | 17, 20 | sylibr 132 |
. . . 4
⊢
(∀𝑥(𝜑 → 𝑥 = 𝑧) → ∀𝑥∀𝑦((𝜑 → 𝑥 = 𝑧) ∧ ([𝑦 / 𝑥]𝜑 → 𝑦 = 𝑧))) |
22 | | prth 336 |
. . . . . 6
⊢ (((𝜑 → 𝑥 = 𝑧) ∧ ([𝑦 / 𝑥]𝜑 → 𝑦 = 𝑧)) → ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑧))) |
23 | | equtr2 1637 |
. . . . . 6
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑧) → 𝑥 = 𝑦) |
24 | 22, 23 | syl6 33 |
. . . . 5
⊢ (((𝜑 → 𝑥 = 𝑧) ∧ ([𝑦 / 𝑥]𝜑 → 𝑦 = 𝑧)) → ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) |
25 | 24 | 2alimi 1385 |
. . . 4
⊢
(∀𝑥∀𝑦((𝜑 → 𝑥 = 𝑧) ∧ ([𝑦 / 𝑥]𝜑 → 𝑦 = 𝑧)) → ∀𝑥∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) |
26 | 21, 25 | syl 14 |
. . 3
⊢
(∀𝑥(𝜑 → 𝑥 = 𝑧) → ∀𝑥∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) |
27 | 26 | exlimiv 1529 |
. 2
⊢
(∃𝑧∀𝑥(𝜑 → 𝑥 = 𝑧) → ∀𝑥∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) |
28 | 9, 27 | sylbir 133 |
1
⊢
(∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦) → ∀𝑥∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) |