Step | Hyp | Ref
| Expression |
1 | | nfv 1619 |
. . . . . 6
⊢ Ⅎw(φ ↔
x = z) |
2 | 1 | sb8 2092 |
. . . . 5
⊢ (∀x(φ ↔ x = z) ↔
∀w[w / x](φ ↔
x = z)) |
3 | | sbbi 2071 |
. . . . . . 7
⊢ ([w / x](φ ↔ x = z) ↔
([w / x]φ ↔
[w / x]x = z)) |
4 | | sb8iota.1 |
. . . . . . . . 9
⊢ Ⅎyφ |
5 | 4 | nfsb 2109 |
. . . . . . . 8
⊢ Ⅎy[w / x]φ |
6 | | equsb3 2102 |
. . . . . . . . 9
⊢ ([w / x]x = z ↔
w = z) |
7 | | nfv 1619 |
. . . . . . . . 9
⊢ Ⅎy w = z |
8 | 6, 7 | nfxfr 1570 |
. . . . . . . 8
⊢ Ⅎy[w / x]x = z |
9 | 5, 8 | nfbi 1834 |
. . . . . . 7
⊢ Ⅎy([w / x]φ ↔
[w / x]x = z) |
10 | 3, 9 | nfxfr 1570 |
. . . . . 6
⊢ Ⅎy[w / x](φ ↔
x = z) |
11 | | nfv 1619 |
. . . . . 6
⊢ Ⅎw[y / x](φ ↔
x = z) |
12 | | sbequ 2060 |
. . . . . 6
⊢ (w = y →
([w / x](φ ↔
x = z)
↔ [y / x](φ ↔
x = z))) |
13 | 10, 11, 12 | cbval 1984 |
. . . . 5
⊢ (∀w[w / x](φ ↔ x = z) ↔
∀y[y / x](φ ↔
x = z)) |
14 | | equsb3 2102 |
. . . . . . 7
⊢ ([y / x]x = z ↔
y = z) |
15 | 14 | sblbis 2072 |
. . . . . 6
⊢ ([y / x](φ ↔ x = z) ↔
([y / x]φ ↔
y = z)) |
16 | 15 | albii 1566 |
. . . . 5
⊢ (∀y[y / x](φ ↔ x = z) ↔
∀y([y / x]φ ↔
y = z)) |
17 | 2, 13, 16 | 3bitri 262 |
. . . 4
⊢ (∀x(φ ↔ x = z) ↔
∀y([y / x]φ ↔
y = z)) |
18 | 17 | abbii 2465 |
. . 3
⊢ {z ∣ ∀x(φ ↔ x = z)} =
{z ∣
∀y([y / x]φ ↔
y = z)} |
19 | 18 | unieqi 3901 |
. 2
⊢ ∪{z ∣ ∀x(φ ↔
x = z)}
= ∪{z ∣ ∀y([y / x]φ ↔
y = z)} |
20 | | dfiota2 4340 |
. 2
⊢ (℩xφ) = ∪{z ∣ ∀x(φ ↔
x = z)} |
21 | | dfiota2 4340 |
. 2
⊢ (℩y[y / x]φ) = ∪{z ∣ ∀y([y / x]φ ↔
y = z)} |
22 | 19, 20, 21 | 3eqtr4i 2383 |
1
⊢ (℩xφ) =
(℩y[y / x]φ) |