Step | Hyp | Ref
| Expression |
1 | | mo23.1 |
. . . . 5
⊢
Ⅎyφ |
2 | | nfv 1418 |
. . . . 5
⊢
Ⅎy x = z |
3 | 1, 2 | nfim 1461 |
. . . 4
⊢
Ⅎy(φ → x = z) |
4 | 3 | nfal 1465 |
. . 3
⊢
Ⅎy∀x(φ → x = z) |
5 | | nfv 1418 |
. . 3
⊢
Ⅎz∀x(φ → x = y) |
6 | | equequ2 1596 |
. . . . 5
⊢ (z = y →
(x = z
↔ x = y)) |
7 | 6 | imbi2d 219 |
. . . 4
⊢ (z = y →
((φ → x = z) ↔
(φ → x = y))) |
8 | 7 | albidv 1702 |
. . 3
⊢ (z = y →
(∀x(φ →
x = z)
↔ ∀x(φ →
x = y))) |
9 | 4, 5, 8 | cbvex 1636 |
. 2
⊢ (∃z∀x(φ → x = z) ↔
∃y∀x(φ → x = y)) |
10 | | nfs1v 1812 |
. . . . . . . 8
⊢
Ⅎx[y / x]φ |
11 | | nfv 1418 |
. . . . . . . 8
⊢
Ⅎx y = z |
12 | 10, 11 | nfim 1461 |
. . . . . . 7
⊢
Ⅎx([y / x]φ → y = z) |
13 | | sbequ2 1649 |
. . . . . . . 8
⊢ (x = y →
([y / x]φ →
φ)) |
14 | | ax-8 1392 |
. . . . . . . 8
⊢ (x = y →
(x = z
→ y = z)) |
15 | 13, 14 | imim12d 68 |
. . . . . . 7
⊢ (x = y →
((φ → x = z) →
([y / x]φ →
y = z))) |
16 | 3, 12, 15 | cbv3 1627 |
. . . . . 6
⊢ (∀x(φ → x = z) →
∀y([y / x]φ →
y = z)) |
17 | 16 | ancli 306 |
. . . . 5
⊢ (∀x(φ → x = z) →
(∀x(φ →
x = z)
∧ ∀y([y / x]φ → y = z))) |
18 | 3 | nfri 1409 |
. . . . . 6
⊢ ((φ → x = z) →
∀y(φ →
x = z)) |
19 | 12 | nfri 1409 |
. . . . . 6
⊢
(([y / x]φ →
y = z)
→ ∀x([y / x]φ →
y = z)) |
20 | 18, 19 | aaanh 1475 |
. . . . 5
⊢ (∀x∀y((φ → x = z) ∧ ([y / x]φ →
y = z))
↔ (∀x(φ →
x = z)
∧ ∀y([y / x]φ → y = z))) |
21 | 17, 20 | sylibr 137 |
. . . 4
⊢ (∀x(φ → x = z) →
∀x∀y((φ → x = z) ∧ ([y / x]φ →
y = z))) |
22 | | prth 326 |
. . . . . 6
⊢ (((φ → x = z) ∧ ([y / x]φ →
y = z))
→ ((φ ∧ [y / x]φ) →
(x = z
∧ y =
z))) |
23 | | equtr2 1594 |
. . . . . 6
⊢
((x = z ∧ y = z) →
x = y) |
24 | 22, 23 | syl6 29 |
. . . . 5
⊢ (((φ → x = z) ∧ ([y / x]φ →
y = z))
→ ((φ ∧ [y / x]φ) →
x = y)) |
25 | 24 | 2alimi 1342 |
. . . 4
⊢ (∀x∀y((φ → x = z) ∧ ([y / x]φ →
y = z))
→ ∀x∀y((φ ∧ [y / x]φ) →
x = y)) |
26 | 21, 25 | syl 14 |
. . 3
⊢ (∀x(φ → x = z) →
∀x∀y((φ ∧
[y / x]φ) →
x = y)) |
27 | 26 | exlimiv 1486 |
. 2
⊢ (∃z∀x(φ → x = z) →
∀x∀y((φ ∧
[y / x]φ) →
x = y)) |
28 | 9, 27 | sylbir 125 |
1
⊢ (∃y∀x(φ → x = y) →
∀x∀y((φ ∧
[y / x]φ) →
x = y)) |