Step | Hyp | Ref
| Expression |
1 | | a9e 1583 |
. 2
⊢ ∃z z = y |
2 | | ax11e 1674 |
. . . . 5
⊢ (x = z →
(∃x(x = z ∧ φ) → ∃zφ)) |
3 | | ax-17 1416 |
. . . . . 6
⊢ (φ → ∀zφ) |
4 | 3 | 19.9h 1531 |
. . . . 5
⊢ (∃zφ ↔ φ) |
5 | 2, 4 | syl6ib 150 |
. . . 4
⊢ (x = z →
(∃x(x = z ∧ φ) → φ)) |
6 | | equequ2 1596 |
. . . . 5
⊢ (z = y →
(x = z
↔ x = y)) |
7 | 6 | anbi1d 438 |
. . . . . . 7
⊢ (z = y →
((x = z
∧ φ)
↔ (x = y ∧ φ))) |
8 | 7 | exbidv 1703 |
. . . . . 6
⊢ (z = y →
(∃x(x = z ∧ φ) ↔ ∃x(x = y ∧ φ))) |
9 | 8 | imbi1d 220 |
. . . . 5
⊢ (z = y →
((∃x(x = z ∧ φ) → φ) ↔ (∃x(x = y ∧ φ) →
φ))) |
10 | 6, 9 | imbi12d 223 |
. . . 4
⊢ (z = y →
((x = z
→ (∃x(x = z ∧ φ) → φ)) ↔ (x = y →
(∃x(x = y ∧ φ) → φ)))) |
11 | 5, 10 | mpbii 136 |
. . 3
⊢ (z = y →
(x = y
→ (∃x(x = y ∧ φ) → φ))) |
12 | 11 | exlimiv 1486 |
. 2
⊢ (∃z z = y →
(x = y
→ (∃x(x = y ∧ φ) → φ))) |
13 | 1, 12 | ax-mp 7 |
1
⊢ (x = y →
(∃x(x = y ∧ φ) → φ)) |