Proof of Theorem ax6e2eq
| Step | Hyp | Ref
| Expression |
| 1 | | ax6ev 1969 |
. . . . . . 7
⊢
∃𝑥 𝑥 = 𝑢 |
| 2 | | hbae 2436 |
. . . . . . . 8
⊢
(∀𝑥 𝑥 = 𝑦 → ∀𝑥∀𝑥 𝑥 = 𝑦) |
| 3 | | ax7 2015 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝑥 = 𝑢 → 𝑦 = 𝑢)) |
| 4 | 3 | sps 2185 |
. . . . . . . . 9
⊢
(∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑢 → 𝑦 = 𝑢)) |
| 5 | 4 | ancld 550 |
. . . . . . . 8
⊢
(∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑢 → (𝑥 = 𝑢 ∧ 𝑦 = 𝑢))) |
| 6 | 2, 5 | eximdh 1864 |
. . . . . . 7
⊢
(∀𝑥 𝑥 = 𝑦 → (∃𝑥 𝑥 = 𝑢 → ∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑢))) |
| 7 | 1, 6 | mpi 20 |
. . . . . 6
⊢
(∀𝑥 𝑥 = 𝑦 → ∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑢)) |
| 8 | 7 | axc4i 2322 |
. . . . 5
⊢
(∀𝑥 𝑥 = 𝑦 → ∀𝑥∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑢)) |
| 9 | | axc11 2435 |
. . . . 5
⊢
(∀𝑥 𝑥 = 𝑦 → (∀𝑥∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → ∀𝑦∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑢))) |
| 10 | 8, 9 | mpd 15 |
. . . 4
⊢
(∀𝑥 𝑥 = 𝑦 → ∀𝑦∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑢)) |
| 11 | | 19.2 1976 |
. . . 4
⊢
(∀𝑦∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → ∃𝑦∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑢)) |
| 12 | 10, 11 | syl 17 |
. . 3
⊢
(∀𝑥 𝑥 = 𝑦 → ∃𝑦∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑢)) |
| 13 | | excomim 2163 |
. . 3
⊢
(∃𝑦∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑢)) |
| 14 | 12, 13 | syl 17 |
. 2
⊢
(∀𝑥 𝑥 = 𝑦 → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑢)) |
| 15 | | equtrr 2021 |
. . . 4
⊢ (𝑢 = 𝑣 → (𝑦 = 𝑢 → 𝑦 = 𝑣)) |
| 16 | 15 | anim2d 612 |
. . 3
⊢ (𝑢 = 𝑣 → ((𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → (𝑥 = 𝑢 ∧ 𝑦 = 𝑣))) |
| 17 | 16 | 2eximdv 1919 |
. 2
⊢ (𝑢 = 𝑣 → (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))) |
| 18 | 14, 17 | syl5com 31 |
1
⊢
(∀𝑥 𝑥 = 𝑦 → (𝑢 = 𝑣 → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))) |