Proof of Theorem ax12v2-o
Step | Hyp | Ref
| Expression |
1 | | ax6ev 1977 |
. 2
⊢
∃𝑧 𝑧 = 𝑦 |
2 | | ax12v2-o.1 |
. . . . 5
⊢ (𝑥 = 𝑧 → (𝜑 → ∀𝑥(𝑥 = 𝑧 → 𝜑))) |
3 | | equequ2 2033 |
. . . . . . 7
⊢ (𝑧 = 𝑦 → (𝑥 = 𝑧 ↔ 𝑥 = 𝑦)) |
4 | 3 | adantl 482 |
. . . . . 6
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ 𝑧 = 𝑦) → (𝑥 = 𝑧 ↔ 𝑥 = 𝑦)) |
5 | | dveeq2-o 36943 |
. . . . . . . . 9
⊢ (¬
∀𝑥 𝑥 = 𝑦 → (𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦)) |
6 | 5 | imp 407 |
. . . . . . . 8
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ 𝑧 = 𝑦) → ∀𝑥 𝑧 = 𝑦) |
7 | | nfa1-o 36925 |
. . . . . . . . 9
⊢
Ⅎ𝑥∀𝑥 𝑧 = 𝑦 |
8 | 3 | imbi1d 342 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑦 → ((𝑥 = 𝑧 → 𝜑) ↔ (𝑥 = 𝑦 → 𝜑))) |
9 | 8 | sps-o 36918 |
. . . . . . . . 9
⊢
(∀𝑥 𝑧 = 𝑦 → ((𝑥 = 𝑧 → 𝜑) ↔ (𝑥 = 𝑦 → 𝜑))) |
10 | 7, 9 | albid 2219 |
. . . . . . . 8
⊢
(∀𝑥 𝑧 = 𝑦 → (∀𝑥(𝑥 = 𝑧 → 𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑))) |
11 | 6, 10 | syl 17 |
. . . . . . 7
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ 𝑧 = 𝑦) → (∀𝑥(𝑥 = 𝑧 → 𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑))) |
12 | 11 | imbi2d 341 |
. . . . . 6
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ 𝑧 = 𝑦) → ((𝜑 → ∀𝑥(𝑥 = 𝑧 → 𝜑)) ↔ (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))) |
13 | 4, 12 | imbi12d 345 |
. . . . 5
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ 𝑧 = 𝑦) → ((𝑥 = 𝑧 → (𝜑 → ∀𝑥(𝑥 = 𝑧 → 𝜑))) ↔ (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))))) |
14 | 2, 13 | mpbii 232 |
. . . 4
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ 𝑧 = 𝑦) → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))) |
15 | 14 | ex 413 |
. . 3
⊢ (¬
∀𝑥 𝑥 = 𝑦 → (𝑧 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))))) |
16 | 15 | exlimdv 1940 |
. 2
⊢ (¬
∀𝑥 𝑥 = 𝑦 → (∃𝑧 𝑧 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))))) |
17 | 1, 16 | mpi 20 |
1
⊢ (¬
∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))) |