Step | Hyp | Ref
| Expression |
1 | | nfv 1418 |
. . . . 5
⊢
Ⅎw(φ ↔ x = z) |
2 | 1 | sb8 1733 |
. . . 4
⊢ (∀x(φ ↔ x = z) ↔
∀w[w / x](φ ↔
x = z)) |
3 | | sbbi 1830 |
. . . . . 6
⊢
([w / x](φ ↔
x = z)
↔ ([w / x]φ ↔
[w / x]x = z)) |
4 | | sb8eu.1 |
. . . . . . . 8
⊢
Ⅎyφ |
5 | 4 | nfsb 1819 |
. . . . . . 7
⊢
Ⅎy[w / x]φ |
6 | | equsb3 1822 |
. . . . . . . 8
⊢
([w / x]x = z ↔ w =
z) |
7 | | nfv 1418 |
. . . . . . . 8
⊢
Ⅎy w = z |
8 | 6, 7 | nfxfr 1360 |
. . . . . . 7
⊢
Ⅎy[w / x]x = z |
9 | 5, 8 | nfbi 1478 |
. . . . . 6
⊢
Ⅎy([w / x]φ ↔ [w / x]x = z) |
10 | 3, 9 | nfxfr 1360 |
. . . . 5
⊢
Ⅎy[w / x](φ ↔ x = z) |
11 | | nfv 1418 |
. . . . 5
⊢
Ⅎw[y / x](φ ↔ x = z) |
12 | | sbequ 1718 |
. . . . 5
⊢ (w = y →
([w / x](φ ↔
x = z)
↔ [y / x](φ ↔
x = z))) |
13 | 10, 11, 12 | cbval 1634 |
. . . 4
⊢ (∀w[w / x](φ ↔ x = z) ↔
∀y[y / x](φ ↔
x = z)) |
14 | | equsb3 1822 |
. . . . . 6
⊢
([y / x]x = z ↔ y =
z) |
15 | 14 | sblbis 1831 |
. . . . 5
⊢
([y / x](φ ↔
x = z)
↔ ([y / x]φ ↔
y = z)) |
16 | 15 | albii 1356 |
. . . 4
⊢ (∀y[y / x](φ ↔ x = z) ↔
∀y([y / x]φ ↔
y = z)) |
17 | 2, 13, 16 | 3bitri 195 |
. . 3
⊢ (∀x(φ ↔ x = z) ↔
∀y([y / x]φ ↔
y = z)) |
18 | 17 | exbii 1493 |
. 2
⊢ (∃z∀x(φ ↔ x = z) ↔
∃z∀y([y / x]φ ↔ y = z)) |
19 | | df-eu 1900 |
. 2
⊢ (∃!xφ ↔ ∃z∀x(φ ↔ x = z)) |
20 | | df-eu 1900 |
. 2
⊢ (∃!y[y / x]φ ↔ ∃z∀y([y / x]φ ↔ y = z)) |
21 | 18, 19, 20 | 3bitr4i 201 |
1
⊢ (∃!xφ ↔ ∃!y[y / x]φ) |