Step | Hyp | Ref
| Expression |
1 | | nfv 1830 |
. . . . 5
⊢
Ⅎ𝑤(𝜑 ↔ 𝑥 = 𝑧) |
2 | 1 | sb8 2412 |
. . . 4
⊢
(∀𝑥(𝜑 ↔ 𝑥 = 𝑧) ↔ ∀𝑤[𝑤 / 𝑥](𝜑 ↔ 𝑥 = 𝑧)) |
3 | | equsb3 2420 |
. . . . . 6
⊢ ([𝑤 / 𝑥]𝑥 = 𝑧 ↔ 𝑤 = 𝑧) |
4 | 3 | sblbis 2392 |
. . . . 5
⊢ ([𝑤 / 𝑥](𝜑 ↔ 𝑥 = 𝑧) ↔ ([𝑤 / 𝑥]𝜑 ↔ 𝑤 = 𝑧)) |
5 | 4 | albii 1737 |
. . . 4
⊢
(∀𝑤[𝑤 / 𝑥](𝜑 ↔ 𝑥 = 𝑧) ↔ ∀𝑤([𝑤 / 𝑥]𝜑 ↔ 𝑤 = 𝑧)) |
6 | | sb8eu.1 |
. . . . . . 7
⊢
Ⅎ𝑦𝜑 |
7 | 6 | nfsb 2428 |
. . . . . 6
⊢
Ⅎ𝑦[𝑤 / 𝑥]𝜑 |
8 | | nfv 1830 |
. . . . . 6
⊢
Ⅎ𝑦 𝑤 = 𝑧 |
9 | 7, 8 | nfbi 1821 |
. . . . 5
⊢
Ⅎ𝑦([𝑤 / 𝑥]𝜑 ↔ 𝑤 = 𝑧) |
10 | | nfv 1830 |
. . . . 5
⊢
Ⅎ𝑤([𝑦 / 𝑥]𝜑 ↔ 𝑦 = 𝑧) |
11 | | sbequ 2364 |
. . . . . 6
⊢ (𝑤 = 𝑦 → ([𝑤 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)) |
12 | | equequ1 1939 |
. . . . . 6
⊢ (𝑤 = 𝑦 → (𝑤 = 𝑧 ↔ 𝑦 = 𝑧)) |
13 | 11, 12 | bibi12d 334 |
. . . . 5
⊢ (𝑤 = 𝑦 → (([𝑤 / 𝑥]𝜑 ↔ 𝑤 = 𝑧) ↔ ([𝑦 / 𝑥]𝜑 ↔ 𝑦 = 𝑧))) |
14 | 9, 10, 13 | cbval 2259 |
. . . 4
⊢
(∀𝑤([𝑤 / 𝑥]𝜑 ↔ 𝑤 = 𝑧) ↔ ∀𝑦([𝑦 / 𝑥]𝜑 ↔ 𝑦 = 𝑧)) |
15 | 2, 5, 14 | 3bitri 285 |
. . 3
⊢
(∀𝑥(𝜑 ↔ 𝑥 = 𝑧) ↔ ∀𝑦([𝑦 / 𝑥]𝜑 ↔ 𝑦 = 𝑧)) |
16 | 15 | exbii 1764 |
. 2
⊢
(∃𝑧∀𝑥(𝜑 ↔ 𝑥 = 𝑧) ↔ ∃𝑧∀𝑦([𝑦 / 𝑥]𝜑 ↔ 𝑦 = 𝑧)) |
17 | | df-eu 2462 |
. 2
⊢
(∃!𝑥𝜑 ↔ ∃𝑧∀𝑥(𝜑 ↔ 𝑥 = 𝑧)) |
18 | | df-eu 2462 |
. 2
⊢
(∃!𝑦[𝑦 / 𝑥]𝜑 ↔ ∃𝑧∀𝑦([𝑦 / 𝑥]𝜑 ↔ 𝑦 = 𝑧)) |
19 | 16, 17, 18 | 3bitr4i 291 |
1
⊢
(∃!𝑥𝜑 ↔ ∃!𝑦[𝑦 / 𝑥]𝜑) |