Step | Hyp | Ref
| Expression |
1 | | nfv 1521 |
. . . . . 6
⊢
Ⅎ𝑧(𝜑 ↔ 𝑥 = 𝑤) |
2 | | nfs1v 1932 |
. . . . . . 7
⊢
Ⅎ𝑥[𝑧 / 𝑥]𝜑 |
3 | | nfv 1521 |
. . . . . . 7
⊢
Ⅎ𝑥 𝑧 = 𝑤 |
4 | 2, 3 | nfbi 1582 |
. . . . . 6
⊢
Ⅎ𝑥([𝑧 / 𝑥]𝜑 ↔ 𝑧 = 𝑤) |
5 | | sbequ12 1764 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → (𝜑 ↔ [𝑧 / 𝑥]𝜑)) |
6 | | equequ1 1705 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → (𝑥 = 𝑤 ↔ 𝑧 = 𝑤)) |
7 | 5, 6 | bibi12d 234 |
. . . . . 6
⊢ (𝑥 = 𝑧 → ((𝜑 ↔ 𝑥 = 𝑤) ↔ ([𝑧 / 𝑥]𝜑 ↔ 𝑧 = 𝑤))) |
8 | 1, 4, 7 | cbval 1747 |
. . . . 5
⊢
(∀𝑥(𝜑 ↔ 𝑥 = 𝑤) ↔ ∀𝑧([𝑧 / 𝑥]𝜑 ↔ 𝑧 = 𝑤)) |
9 | | cbviota.2 |
. . . . . . . 8
⊢
Ⅎ𝑦𝜑 |
10 | 9 | nfsb 1939 |
. . . . . . 7
⊢
Ⅎ𝑦[𝑧 / 𝑥]𝜑 |
11 | | nfv 1521 |
. . . . . . 7
⊢
Ⅎ𝑦 𝑧 = 𝑤 |
12 | 10, 11 | nfbi 1582 |
. . . . . 6
⊢
Ⅎ𝑦([𝑧 / 𝑥]𝜑 ↔ 𝑧 = 𝑤) |
13 | | nfv 1521 |
. . . . . 6
⊢
Ⅎ𝑧(𝜓 ↔ 𝑦 = 𝑤) |
14 | | sbequ 1833 |
. . . . . . . 8
⊢ (𝑧 = 𝑦 → ([𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)) |
15 | | cbviota.3 |
. . . . . . . . 9
⊢
Ⅎ𝑥𝜓 |
16 | | cbviota.1 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) |
17 | 15, 16 | sbie 1784 |
. . . . . . . 8
⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓) |
18 | 14, 17 | bitrdi 195 |
. . . . . . 7
⊢ (𝑧 = 𝑦 → ([𝑧 / 𝑥]𝜑 ↔ 𝜓)) |
19 | | equequ1 1705 |
. . . . . . 7
⊢ (𝑧 = 𝑦 → (𝑧 = 𝑤 ↔ 𝑦 = 𝑤)) |
20 | 18, 19 | bibi12d 234 |
. . . . . 6
⊢ (𝑧 = 𝑦 → (([𝑧 / 𝑥]𝜑 ↔ 𝑧 = 𝑤) ↔ (𝜓 ↔ 𝑦 = 𝑤))) |
21 | 12, 13, 20 | cbval 1747 |
. . . . 5
⊢
(∀𝑧([𝑧 / 𝑥]𝜑 ↔ 𝑧 = 𝑤) ↔ ∀𝑦(𝜓 ↔ 𝑦 = 𝑤)) |
22 | 8, 21 | bitri 183 |
. . . 4
⊢
(∀𝑥(𝜑 ↔ 𝑥 = 𝑤) ↔ ∀𝑦(𝜓 ↔ 𝑦 = 𝑤)) |
23 | 22 | abbii 2286 |
. . 3
⊢ {𝑤 ∣ ∀𝑥(𝜑 ↔ 𝑥 = 𝑤)} = {𝑤 ∣ ∀𝑦(𝜓 ↔ 𝑦 = 𝑤)} |
24 | 23 | unieqi 3804 |
. 2
⊢ ∪ {𝑤
∣ ∀𝑥(𝜑 ↔ 𝑥 = 𝑤)} = ∪ {𝑤 ∣ ∀𝑦(𝜓 ↔ 𝑦 = 𝑤)} |
25 | | dfiota2 5159 |
. 2
⊢
(℩𝑥𝜑) = ∪
{𝑤 ∣ ∀𝑥(𝜑 ↔ 𝑥 = 𝑤)} |
26 | | dfiota2 5159 |
. 2
⊢
(℩𝑦𝜓) = ∪
{𝑤 ∣ ∀𝑦(𝜓 ↔ 𝑦 = 𝑤)} |
27 | 24, 25, 26 | 3eqtr4i 2201 |
1
⊢
(℩𝑥𝜑) = (℩𝑦𝜓) |