| Step | Hyp | Ref
| Expression |
| 1 | | nfa1 2151 |
. . 3
⊢
Ⅎ𝑥∀𝑥Ⅎ𝑦𝜑 |
| 2 | | nfmo1 2557 |
. . 3
⊢
Ⅎ𝑥∃*𝑥𝜑 |
| 3 | | nfnf1 2154 |
. . . . . . 7
⊢
Ⅎ𝑦Ⅎ𝑦𝜑 |
| 4 | 3 | nfal 2323 |
. . . . . 6
⊢
Ⅎ𝑦∀𝑥Ⅎ𝑦𝜑 |
| 5 | | sp 2183 |
. . . . . . 7
⊢
(∀𝑥Ⅎ𝑦𝜑 → Ⅎ𝑦𝜑) |
| 6 | 1, 5 | nfmodv 2559 |
. . . . . 6
⊢
(∀𝑥Ⅎ𝑦𝜑 → Ⅎ𝑦∃*𝑥𝜑) |
| 7 | 4, 6 | nfan1 2200 |
. . . . 5
⊢
Ⅎ𝑦(∀𝑥Ⅎ𝑦𝜑 ∧ ∃*𝑥𝜑) |
| 8 | | df-mo 2540 |
. . . . . . 7
⊢
(∃*𝑥𝜑 ↔ ∃𝑢∀𝑥(𝜑 → 𝑥 = 𝑢)) |
| 9 | | sp 2183 |
. . . . . . . . . 10
⊢
(∀𝑥(𝜑 → 𝑥 = 𝑢) → (𝜑 → 𝑥 = 𝑢)) |
| 10 | | spsbim 2072 |
. . . . . . . . . . 11
⊢
(∀𝑥(𝜑 → 𝑥 = 𝑢) → ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝑥 = 𝑢)) |
| 11 | | equsb3 2103 |
. . . . . . . . . . 11
⊢ ([𝑦 / 𝑥]𝑥 = 𝑢 ↔ 𝑦 = 𝑢) |
| 12 | 10, 11 | imbitrdi 251 |
. . . . . . . . . 10
⊢
(∀𝑥(𝜑 → 𝑥 = 𝑢) → ([𝑦 / 𝑥]𝜑 → 𝑦 = 𝑢)) |
| 13 | 9, 12 | anim12d 609 |
. . . . . . . . 9
⊢
(∀𝑥(𝜑 → 𝑥 = 𝑢) → ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → (𝑥 = 𝑢 ∧ 𝑦 = 𝑢))) |
| 14 | | equtr2 2026 |
. . . . . . . . 9
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑢) → 𝑥 = 𝑦) |
| 15 | 13, 14 | syl6 35 |
. . . . . . . 8
⊢
(∀𝑥(𝜑 → 𝑥 = 𝑢) → ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) |
| 16 | 15 | exlimiv 1930 |
. . . . . . 7
⊢
(∃𝑢∀𝑥(𝜑 → 𝑥 = 𝑢) → ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) |
| 17 | 8, 16 | sylbi 217 |
. . . . . 6
⊢
(∃*𝑥𝜑 → ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) |
| 18 | 17 | adantl 481 |
. . . . 5
⊢
((∀𝑥Ⅎ𝑦𝜑 ∧ ∃*𝑥𝜑) → ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) |
| 19 | 7, 18 | alrimi 2213 |
. . . 4
⊢
((∀𝑥Ⅎ𝑦𝜑 ∧ ∃*𝑥𝜑) → ∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) |
| 20 | 19 | ex 412 |
. . 3
⊢
(∀𝑥Ⅎ𝑦𝜑 → (∃*𝑥𝜑 → ∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))) |
| 21 | 1, 2, 20 | alrimd 2215 |
. 2
⊢
(∀𝑥Ⅎ𝑦𝜑 → (∃*𝑥𝜑 → ∀𝑥∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))) |
| 22 | | nfa1 2151 |
. . . . . 6
⊢
Ⅎ𝑥∀𝑥((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) |
| 23 | | nfs1v 2156 |
. . . . . 6
⊢
Ⅎ𝑥[𝑦 / 𝑥]𝜑 |
| 24 | | pm3.3 448 |
. . . . . . . 8
⊢ (((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) → (𝜑 → ([𝑦 / 𝑥]𝜑 → 𝑥 = 𝑦))) |
| 25 | 24 | com23 86 |
. . . . . . 7
⊢ (((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) → ([𝑦 / 𝑥]𝜑 → (𝜑 → 𝑥 = 𝑦))) |
| 26 | 25 | sps 2185 |
. . . . . 6
⊢
(∀𝑥((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) → ([𝑦 / 𝑥]𝜑 → (𝜑 → 𝑥 = 𝑦))) |
| 27 | 22, 23, 26 | alrimd 2215 |
. . . . 5
⊢
(∀𝑥((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) → ([𝑦 / 𝑥]𝜑 → ∀𝑥(𝜑 → 𝑥 = 𝑦))) |
| 28 | 27 | aleximi 1832 |
. . . 4
⊢
(∀𝑦∀𝑥((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) → (∃𝑦[𝑦 / 𝑥]𝜑 → ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦))) |
| 29 | 28 | alcoms 2158 |
. . 3
⊢
(∀𝑥∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) → (∃𝑦[𝑦 / 𝑥]𝜑 → ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦))) |
| 30 | | moabs 2543 |
. . . 4
⊢
(∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃*𝑥𝜑)) |
| 31 | | wl-sb8eft 37552 |
. . . . 5
⊢
(∀𝑥Ⅎ𝑦𝜑 → (∃𝑥𝜑 ↔ ∃𝑦[𝑦 / 𝑥]𝜑)) |
| 32 | | wl-mo2t 37576 |
. . . . 5
⊢
(∀𝑥Ⅎ𝑦𝜑 → (∃*𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦))) |
| 33 | 31, 32 | imbi12d 344 |
. . . 4
⊢
(∀𝑥Ⅎ𝑦𝜑 → ((∃𝑥𝜑 → ∃*𝑥𝜑) ↔ (∃𝑦[𝑦 / 𝑥]𝜑 → ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦)))) |
| 34 | 30, 33 | bitrid 283 |
. . 3
⊢
(∀𝑥Ⅎ𝑦𝜑 → (∃*𝑥𝜑 ↔ (∃𝑦[𝑦 / 𝑥]𝜑 → ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦)))) |
| 35 | 29, 34 | imbitrrid 246 |
. 2
⊢
(∀𝑥Ⅎ𝑦𝜑 → (∀𝑥∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) → ∃*𝑥𝜑)) |
| 36 | 21, 35 | impbid 212 |
1
⊢
(∀𝑥Ⅎ𝑦𝜑 → (∃*𝑥𝜑 ↔ ∀𝑥∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))) |