Step | Hyp | Ref
| Expression |
1 | | eu6 2575 |
. 2
⊢
(∃!𝑥𝜓 ↔ ∃𝑢∀𝑥(𝜓 ↔ 𝑥 = 𝑢)) |
2 | | wl-eudf.2 |
. . 3
⊢
Ⅎ𝑦𝜑 |
3 | | wl-eudf.1 |
. . . 4
⊢
Ⅎ𝑥𝜑 |
4 | | wl-eudf.4 |
. . . . 5
⊢ (𝜑 → Ⅎ𝑦𝜓) |
5 | | wl-eudf.3 |
. . . . . 6
⊢ (𝜑 → ¬ ∀𝑥 𝑥 = 𝑦) |
6 | | nfeqf1 2380 |
. . . . . . 7
⊢ (¬
∀𝑦 𝑦 = 𝑥 → Ⅎ𝑦 𝑥 = 𝑢) |
7 | 6 | naecoms 2430 |
. . . . . 6
⊢ (¬
∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦 𝑥 = 𝑢) |
8 | 5, 7 | syl 17 |
. . . . 5
⊢ (𝜑 → Ⅎ𝑦 𝑥 = 𝑢) |
9 | 4, 8 | nfbid 1908 |
. . . 4
⊢ (𝜑 → Ⅎ𝑦(𝜓 ↔ 𝑥 = 𝑢)) |
10 | 3, 9 | nfald 2325 |
. . 3
⊢ (𝜑 → Ⅎ𝑦∀𝑥(𝜓 ↔ 𝑥 = 𝑢)) |
11 | | nfnae 2435 |
. . . . . . 7
⊢
Ⅎ𝑥 ¬
∀𝑥 𝑥 = 𝑦 |
12 | | nfeqf2 2378 |
. . . . . . 7
⊢ (¬
∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥 𝑢 = 𝑦) |
13 | 11, 12 | nfan1 2196 |
. . . . . 6
⊢
Ⅎ𝑥(¬
∀𝑥 𝑥 = 𝑦 ∧ 𝑢 = 𝑦) |
14 | | equequ2 2032 |
. . . . . . . 8
⊢ (𝑢 = 𝑦 → (𝑥 = 𝑢 ↔ 𝑥 = 𝑦)) |
15 | 14 | bibi2d 342 |
. . . . . . 7
⊢ (𝑢 = 𝑦 → ((𝜓 ↔ 𝑥 = 𝑢) ↔ (𝜓 ↔ 𝑥 = 𝑦))) |
16 | 15 | adantl 481 |
. . . . . 6
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ 𝑢 = 𝑦) → ((𝜓 ↔ 𝑥 = 𝑢) ↔ (𝜓 ↔ 𝑥 = 𝑦))) |
17 | 13, 16 | albid 2218 |
. . . . 5
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ 𝑢 = 𝑦) → (∀𝑥(𝜓 ↔ 𝑥 = 𝑢) ↔ ∀𝑥(𝜓 ↔ 𝑥 = 𝑦))) |
18 | 5, 17 | sylan 579 |
. . . 4
⊢ ((𝜑 ∧ 𝑢 = 𝑦) → (∀𝑥(𝜓 ↔ 𝑥 = 𝑢) ↔ ∀𝑥(𝜓 ↔ 𝑥 = 𝑦))) |
19 | 18 | ex 412 |
. . 3
⊢ (𝜑 → (𝑢 = 𝑦 → (∀𝑥(𝜓 ↔ 𝑥 = 𝑢) ↔ ∀𝑥(𝜓 ↔ 𝑥 = 𝑦)))) |
20 | 2, 10, 19 | cbvexd 2409 |
. 2
⊢ (𝜑 → (∃𝑢∀𝑥(𝜓 ↔ 𝑥 = 𝑢) ↔ ∃𝑦∀𝑥(𝜓 ↔ 𝑥 = 𝑦))) |
21 | 1, 20 | syl5bb 282 |
1
⊢ (𝜑 → (∃!𝑥𝜓 ↔ ∃𝑦∀𝑥(𝜓 ↔ 𝑥 = 𝑦))) |