Step | Hyp | Ref
| Expression |
1 | | a9e 1583 |
. 2
⊢ ∃z z = y |
2 | | dveeq2or 1694 |
. . . . . 6
⊢ (∀x x = y ∨ Ⅎx
z = y) |
3 | | nfnf1 1433 |
. . . . . . . . . . 11
⊢
ℲxℲx z = y |
4 | 3 | nfri 1409 |
. . . . . . . . . 10
⊢
(Ⅎx z = y →
∀xℲx
z = y) |
5 | | ax11v 1705 |
. . . . . . . . . . . . 13
⊢ (x = z →
(φ → ∀x(x = z →
φ))) |
6 | | equequ2 1596 |
. . . . . . . . . . . . . . 15
⊢ (z = y →
(x = z
↔ x = y)) |
7 | 6 | adantl 262 |
. . . . . . . . . . . . . 14
⊢
((Ⅎx z = y ∧ z = y) → (x =
z ↔ x = y)) |
8 | | nfr 1408 |
. . . . . . . . . . . . . . . . 17
⊢
(Ⅎx z = y →
(z = y
→ ∀x z = y)) |
9 | 8 | imp 115 |
. . . . . . . . . . . . . . . 16
⊢
((Ⅎx z = y ∧ z = y) → ∀x z = y) |
10 | | hba1 1430 |
. . . . . . . . . . . . . . . . 17
⊢ (∀x z = y →
∀x∀x z = y) |
11 | 6 | imbi1d 220 |
. . . . . . . . . . . . . . . . . 18
⊢ (z = y →
((x = z
→ φ) ↔ (x = y →
φ))) |
12 | 11 | sps 1427 |
. . . . . . . . . . . . . . . . 17
⊢ (∀x z = y →
((x = z
→ φ) ↔ (x = y →
φ))) |
13 | 10, 12 | albidh 1366 |
. . . . . . . . . . . . . . . 16
⊢ (∀x z = y →
(∀x(x = z → φ)
↔ ∀x(x = y → φ))) |
14 | 9, 13 | syl 14 |
. . . . . . . . . . . . . . 15
⊢
((Ⅎx z = y ∧ z = y) → (∀x(x = z →
φ) ↔ ∀x(x = y →
φ))) |
15 | 14 | imbi2d 219 |
. . . . . . . . . . . . . 14
⊢
((Ⅎx z = y ∧ z = y) → ((φ → ∀x(x = z →
φ)) ↔ (φ → ∀x(x = y →
φ)))) |
16 | 7, 15 | imbi12d 223 |
. . . . . . . . . . . . 13
⊢
((Ⅎx z = y ∧ z = y) → ((x =
z → (φ → ∀x(x = z →
φ))) ↔ (x = y →
(φ → ∀x(x = y →
φ))))) |
17 | 5, 16 | mpbii 136 |
. . . . . . . . . . . 12
⊢
((Ⅎx z = y ∧ z = y) → (x =
y → (φ → ∀x(x = y →
φ)))) |
18 | 17 | ex 108 |
. . . . . . . . . . 11
⊢
(Ⅎx z = y →
(z = y
→ (x = y → (φ
→ ∀x(x = y → φ))))) |
19 | 18 | imp4a 331 |
. . . . . . . . . 10
⊢
(Ⅎx z = y →
(z = y
→ ((x = y ∧ φ) → ∀x(x = y →
φ)))) |
20 | 4, 19 | alrimih 1355 |
. . . . . . . . 9
⊢
(Ⅎx z = y →
∀x(z = y → ((x =
y ∧ φ) → ∀x(x = y →
φ)))) |
21 | | 19.21t 1471 |
. . . . . . . . 9
⊢
(Ⅎx z = y →
(∀x(z = y → ((x =
y ∧ φ) → ∀x(x = y →
φ))) ↔ (z = y →
∀x((x = y ∧ φ) → ∀x(x = y →
φ))))) |
22 | 20, 21 | mpbid 135 |
. . . . . . . 8
⊢
(Ⅎx z = y →
(z = y
→ ∀x((x = y ∧ φ) → ∀x(x = y →
φ)))) |
23 | | hba1 1430 |
. . . . . . . . 9
⊢ (∀x(x = y →
φ) → ∀x∀x(x = y →
φ)) |
24 | 23 | 19.23h 1384 |
. . . . . . . 8
⊢ (∀x((x = y ∧ φ) →
∀x(x = y → φ))
↔ (∃x(x = y ∧ φ) → ∀x(x = y →
φ))) |
25 | 22, 24 | syl6ib 150 |
. . . . . . 7
⊢
(Ⅎx z = y →
(z = y
→ (∃x(x = y ∧ φ) → ∀x(x = y →
φ)))) |
26 | 25 | orim2i 677 |
. . . . . 6
⊢ ((∀x x = y ∨ Ⅎx
z = y)
→ (∀x x = y ∨ (z = y →
(∃x(x = y ∧ φ) → ∀x(x = y →
φ))))) |
27 | 2, 26 | ax-mp 7 |
. . . . 5
⊢ (∀x x = y ∨ (z = y → (∃x(x = y ∧ φ) →
∀x(x = y → φ)))) |
28 | | pm2.76 720 |
. . . . 5
⊢ ((∀x x = y ∨ (z = y → (∃x(x = y ∧ φ) →
∀x(x = y → φ)))) → ((∀x x = y ∨ z = y) → (∀x x = y ∨ (∃x(x = y ∧ φ) → ∀x(x = y →
φ))))) |
29 | 27, 28 | ax-mp 7 |
. . . 4
⊢ ((∀x x = y ∨ z = y) → (∀x x = y ∨ (∃x(x = y ∧ φ) → ∀x(x = y →
φ)))) |
30 | 29 | olcs 654 |
. . 3
⊢ (z = y →
(∀x
x = y
∨ (∃x(x = y ∧ φ) →
∀x(x = y → φ)))) |
31 | 30 | exlimiv 1486 |
. 2
⊢ (∃z z = y →
(∀x
x = y
∨ (∃x(x = y ∧ φ) →
∀x(x = y → φ)))) |
32 | 1, 31 | ax-mp 7 |
1
⊢ (∀x x = y ∨ (∃x(x = y ∧ φ) → ∀x(x = y →
φ))) |