Step | Hyp | Ref
| Expression |
1 | | a9e 1689 |
. 2
⊢
∃𝑧 𝑧 = 𝑦 |
2 | | ax11e 1789 |
. . . . 5
⊢ (𝑥 = 𝑧 → (∃𝑥(𝑥 = 𝑧 ∧ 𝜑) → ∃𝑧𝜑)) |
3 | | ax-17 1519 |
. . . . . 6
⊢ (𝜑 → ∀𝑧𝜑) |
4 | 3 | 19.9h 1636 |
. . . . 5
⊢
(∃𝑧𝜑 ↔ 𝜑) |
5 | 2, 4 | syl6ib 160 |
. . . 4
⊢ (𝑥 = 𝑧 → (∃𝑥(𝑥 = 𝑧 ∧ 𝜑) → 𝜑)) |
6 | | equequ2 1706 |
. . . . 5
⊢ (𝑧 = 𝑦 → (𝑥 = 𝑧 ↔ 𝑥 = 𝑦)) |
7 | 6 | anbi1d 462 |
. . . . . . 7
⊢ (𝑧 = 𝑦 → ((𝑥 = 𝑧 ∧ 𝜑) ↔ (𝑥 = 𝑦 ∧ 𝜑))) |
8 | 7 | exbidv 1818 |
. . . . . 6
⊢ (𝑧 = 𝑦 → (∃𝑥(𝑥 = 𝑧 ∧ 𝜑) ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) |
9 | 8 | imbi1d 230 |
. . . . 5
⊢ (𝑧 = 𝑦 → ((∃𝑥(𝑥 = 𝑧 ∧ 𝜑) → 𝜑) ↔ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → 𝜑))) |
10 | 6, 9 | imbi12d 233 |
. . . 4
⊢ (𝑧 = 𝑦 → ((𝑥 = 𝑧 → (∃𝑥(𝑥 = 𝑧 ∧ 𝜑) → 𝜑)) ↔ (𝑥 = 𝑦 → (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → 𝜑)))) |
11 | 5, 10 | mpbii 147 |
. . 3
⊢ (𝑧 = 𝑦 → (𝑥 = 𝑦 → (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → 𝜑))) |
12 | 11 | exlimiv 1591 |
. 2
⊢
(∃𝑧 𝑧 = 𝑦 → (𝑥 = 𝑦 → (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → 𝜑))) |
13 | 1, 12 | ax-mp 5 |
1
⊢ (𝑥 = 𝑦 → (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → 𝜑)) |