Proof of Theorem pm14.24
Step | Hyp | Ref
| Expression |
1 | | nfeu1 2589 |
. . . . 5
⊢
Ⅎ𝑥∃!𝑥𝜑 |
2 | | nfsbc1v 3700 |
. . . . 5
⊢
Ⅎ𝑥[𝑦 / 𝑥]𝜑 |
3 | | pm14.12 41577 |
. . . . . . . . . 10
⊢
(∃!𝑥𝜑 → ∀𝑥∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) |
4 | 3 | 19.21bbi 2191 |
. . . . . . . . 9
⊢
(∃!𝑥𝜑 → ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) |
5 | 4 | ancomsd 469 |
. . . . . . . 8
⊢
(∃!𝑥𝜑 → (([𝑦 / 𝑥]𝜑 ∧ 𝜑) → 𝑥 = 𝑦)) |
6 | 5 | expdimp 456 |
. . . . . . 7
⊢
((∃!𝑥𝜑 ∧ [𝑦 / 𝑥]𝜑) → (𝜑 → 𝑥 = 𝑦)) |
7 | | pm13.13b 41564 |
. . . . . . . . 9
⊢
(([𝑦 / 𝑥]𝜑 ∧ 𝑥 = 𝑦) → 𝜑) |
8 | 7 | ex 416 |
. . . . . . . 8
⊢
([𝑦 / 𝑥]𝜑 → (𝑥 = 𝑦 → 𝜑)) |
9 | 8 | adantl 485 |
. . . . . . 7
⊢
((∃!𝑥𝜑 ∧ [𝑦 / 𝑥]𝜑) → (𝑥 = 𝑦 → 𝜑)) |
10 | 6, 9 | impbid 215 |
. . . . . 6
⊢
((∃!𝑥𝜑 ∧ [𝑦 / 𝑥]𝜑) → (𝜑 ↔ 𝑥 = 𝑦)) |
11 | 10 | ex 416 |
. . . . 5
⊢
(∃!𝑥𝜑 → ([𝑦 / 𝑥]𝜑 → (𝜑 ↔ 𝑥 = 𝑦))) |
12 | 1, 2, 11 | alrimd 2217 |
. . . 4
⊢
(∃!𝑥𝜑 → ([𝑦 / 𝑥]𝜑 → ∀𝑥(𝜑 ↔ 𝑥 = 𝑦))) |
13 | | iotaval 6313 |
. . . . 5
⊢
(∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → (℩𝑥𝜑) = 𝑦) |
14 | 13 | eqcomd 2744 |
. . . 4
⊢
(∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → 𝑦 = (℩𝑥𝜑)) |
15 | 12, 14 | syl6 35 |
. . 3
⊢
(∃!𝑥𝜑 → ([𝑦 / 𝑥]𝜑 → 𝑦 = (℩𝑥𝜑))) |
16 | | iota4 6320 |
. . . 4
⊢
(∃!𝑥𝜑 → [(℩𝑥𝜑) / 𝑥]𝜑) |
17 | | dfsbcq 3682 |
. . . 4
⊢ (𝑦 = (℩𝑥𝜑) → ([𝑦 / 𝑥]𝜑 ↔ [(℩𝑥𝜑) / 𝑥]𝜑)) |
18 | 16, 17 | syl5ibrcom 250 |
. . 3
⊢
(∃!𝑥𝜑 → (𝑦 = (℩𝑥𝜑) → [𝑦 / 𝑥]𝜑)) |
19 | 15, 18 | impbid 215 |
. 2
⊢
(∃!𝑥𝜑 → ([𝑦 / 𝑥]𝜑 ↔ 𝑦 = (℩𝑥𝜑))) |
20 | 19 | alrimiv 1934 |
1
⊢
(∃!𝑥𝜑 → ∀𝑦([𝑦 / 𝑥]𝜑 ↔ 𝑦 = (℩𝑥𝜑))) |