Step | Hyp | Ref
| Expression |
1 | | nfnf1 2155 |
. . . . . 6
⊢
Ⅎ𝑦Ⅎ𝑦𝜑 |
2 | 1 | nfal 2322 |
. . . . 5
⊢
Ⅎ𝑦∀𝑥Ⅎ𝑦𝜑 |
3 | | equsb3 2105 |
. . . . . . 7
⊢ ([𝑣 / 𝑥]𝑥 = 𝑢 ↔ 𝑣 = 𝑢) |
4 | 3 | sblbis 2310 |
. . . . . 6
⊢ ([𝑣 / 𝑥](𝜑 ↔ 𝑥 = 𝑢) ↔ ([𝑣 / 𝑥]𝜑 ↔ 𝑣 = 𝑢)) |
5 | | nfa1 2152 |
. . . . . . . 8
⊢
Ⅎ𝑥∀𝑥Ⅎ𝑦𝜑 |
6 | | sp 2180 |
. . . . . . . 8
⊢
(∀𝑥Ⅎ𝑦𝜑 → Ⅎ𝑦𝜑) |
7 | 5, 6 | nfsbd 2525 |
. . . . . . 7
⊢
(∀𝑥Ⅎ𝑦𝜑 → Ⅎ𝑦[𝑣 / 𝑥]𝜑) |
8 | | nfvd 1923 |
. . . . . . 7
⊢
(∀𝑥Ⅎ𝑦𝜑 → Ⅎ𝑦 𝑣 = 𝑢) |
9 | 7, 8 | nfbid 1910 |
. . . . . 6
⊢
(∀𝑥Ⅎ𝑦𝜑 → Ⅎ𝑦([𝑣 / 𝑥]𝜑 ↔ 𝑣 = 𝑢)) |
10 | 4, 9 | nfxfrd 1861 |
. . . . 5
⊢
(∀𝑥Ⅎ𝑦𝜑 → Ⅎ𝑦[𝑣 / 𝑥](𝜑 ↔ 𝑥 = 𝑢)) |
11 | | sbequ 2089 |
. . . . . 6
⊢ (𝑣 = 𝑦 → ([𝑣 / 𝑥](𝜑 ↔ 𝑥 = 𝑢) ↔ [𝑦 / 𝑥](𝜑 ↔ 𝑥 = 𝑢))) |
12 | 11 | a1i 11 |
. . . . 5
⊢
(∀𝑥Ⅎ𝑦𝜑 → (𝑣 = 𝑦 → ([𝑣 / 𝑥](𝜑 ↔ 𝑥 = 𝑢) ↔ [𝑦 / 𝑥](𝜑 ↔ 𝑥 = 𝑢)))) |
13 | 2, 10, 12 | cbvald 2406 |
. . . 4
⊢
(∀𝑥Ⅎ𝑦𝜑 → (∀𝑣[𝑣 / 𝑥](𝜑 ↔ 𝑥 = 𝑢) ↔ ∀𝑦[𝑦 / 𝑥](𝜑 ↔ 𝑥 = 𝑢))) |
14 | | nfv 1922 |
. . . . . 6
⊢
Ⅎ𝑣(𝜑 ↔ 𝑥 = 𝑢) |
15 | 14 | sb8 2520 |
. . . . 5
⊢
(∀𝑥(𝜑 ↔ 𝑥 = 𝑢) ↔ ∀𝑣[𝑣 / 𝑥](𝜑 ↔ 𝑥 = 𝑢)) |
16 | 15 | bicomi 227 |
. . . 4
⊢
(∀𝑣[𝑣 / 𝑥](𝜑 ↔ 𝑥 = 𝑢) ↔ ∀𝑥(𝜑 ↔ 𝑥 = 𝑢)) |
17 | | equsb3 2105 |
. . . . . 6
⊢ ([𝑦 / 𝑥]𝑥 = 𝑢 ↔ 𝑦 = 𝑢) |
18 | 17 | sblbis 2310 |
. . . . 5
⊢ ([𝑦 / 𝑥](𝜑 ↔ 𝑥 = 𝑢) ↔ ([𝑦 / 𝑥]𝜑 ↔ 𝑦 = 𝑢)) |
19 | 18 | albii 1827 |
. . . 4
⊢
(∀𝑦[𝑦 / 𝑥](𝜑 ↔ 𝑥 = 𝑢) ↔ ∀𝑦([𝑦 / 𝑥]𝜑 ↔ 𝑦 = 𝑢)) |
20 | 13, 16, 19 | 3bitr3g 316 |
. . 3
⊢
(∀𝑥Ⅎ𝑦𝜑 → (∀𝑥(𝜑 ↔ 𝑥 = 𝑢) ↔ ∀𝑦([𝑦 / 𝑥]𝜑 ↔ 𝑦 = 𝑢))) |
21 | 20 | exbidv 1929 |
. 2
⊢
(∀𝑥Ⅎ𝑦𝜑 → (∃𝑢∀𝑥(𝜑 ↔ 𝑥 = 𝑢) ↔ ∃𝑢∀𝑦([𝑦 / 𝑥]𝜑 ↔ 𝑦 = 𝑢))) |
22 | | eu6 2573 |
. 2
⊢
(∃!𝑥𝜑 ↔ ∃𝑢∀𝑥(𝜑 ↔ 𝑥 = 𝑢)) |
23 | | eu6 2573 |
. 2
⊢
(∃!𝑦[𝑦 / 𝑥]𝜑 ↔ ∃𝑢∀𝑦([𝑦 / 𝑥]𝜑 ↔ 𝑦 = 𝑢)) |
24 | 21, 22, 23 | 3bitr4g 317 |
1
⊢
(∀𝑥Ⅎ𝑦𝜑 → (∃!𝑥𝜑 ↔ ∃!𝑦[𝑦 / 𝑥]𝜑)) |