Step | Hyp | Ref
| Expression |
1 | | nfv 1508 |
. 2
⊢
Ⅎ𝑧𝜑 |
2 | | df-clab 2144 |
. . 3
⊢ (𝑧 ∈ {𝑦 ∣ 𝜓} ↔ [𝑧 / 𝑦]𝜓) |
3 | | nfabdw.1 |
. . . . 5
⊢
Ⅎ𝑦𝜑 |
4 | | nfabdw.2 |
. . . . 5
⊢ (𝜑 → Ⅎ𝑥𝜓) |
5 | 3, 4 | alrimi 1502 |
. . . 4
⊢ (𝜑 → ∀𝑦Ⅎ𝑥𝜓) |
6 | | nfa1 1521 |
. . . . . . . . 9
⊢
Ⅎ𝑦∀𝑦Ⅎ𝑥𝜓 |
7 | | sb6 1866 |
. . . . . . . . . . . 12
⊢ ([𝑧 / 𝑦]𝜓 ↔ ∀𝑦(𝑦 = 𝑧 → 𝜓)) |
8 | 7 | a1i 9 |
. . . . . . . . . . 11
⊢
(∀𝑦Ⅎ𝑥𝜓 → ([𝑧 / 𝑦]𝜓 ↔ ∀𝑦(𝑦 = 𝑧 → 𝜓))) |
9 | 7 | biimpri 132 |
. . . . . . . . . . . 12
⊢
(∀𝑦(𝑦 = 𝑧 → 𝜓) → [𝑧 / 𝑦]𝜓) |
10 | 9 | axc4i 1522 |
. . . . . . . . . . 11
⊢
(∀𝑦(𝑦 = 𝑧 → 𝜓) → ∀𝑦[𝑧 / 𝑦]𝜓) |
11 | 8, 10 | syl6bi 162 |
. . . . . . . . . 10
⊢
(∀𝑦Ⅎ𝑥𝜓 → ([𝑧 / 𝑦]𝜓 → ∀𝑦[𝑧 / 𝑦]𝜓)) |
12 | 6, 11 | nf5d 2005 |
. . . . . . . . 9
⊢
(∀𝑦Ⅎ𝑥𝜓 → Ⅎ𝑦[𝑧 / 𝑦]𝜓) |
13 | 6, 12 | nfim1 1551 |
. . . . . . . 8
⊢
Ⅎ𝑦(∀𝑦Ⅎ𝑥𝜓 → [𝑧 / 𝑦]𝜓) |
14 | | sbequ12 1751 |
. . . . . . . . 9
⊢ (𝑦 = 𝑧 → (𝜓 ↔ [𝑧 / 𝑦]𝜓)) |
15 | 14 | imbi2d 229 |
. . . . . . . 8
⊢ (𝑦 = 𝑧 → ((∀𝑦Ⅎ𝑥𝜓 → 𝜓) ↔ (∀𝑦Ⅎ𝑥𝜓 → [𝑧 / 𝑦]𝜓))) |
16 | 13, 15 | equsalv 1773 |
. . . . . . 7
⊢
(∀𝑦(𝑦 = 𝑧 → (∀𝑦Ⅎ𝑥𝜓 → 𝜓)) ↔ (∀𝑦Ⅎ𝑥𝜓 → [𝑧 / 𝑦]𝜓)) |
17 | 16 | bicomi 131 |
. . . . . 6
⊢
((∀𝑦Ⅎ𝑥𝜓 → [𝑧 / 𝑦]𝜓) ↔ ∀𝑦(𝑦 = 𝑧 → (∀𝑦Ⅎ𝑥𝜓 → 𝜓))) |
18 | | nfv 1508 |
. . . . . . . 8
⊢
Ⅎ𝑥 𝑦 = 𝑧 |
19 | | nfnf1 1524 |
. . . . . . . . . 10
⊢
Ⅎ𝑥Ⅎ𝑥𝜓 |
20 | 19 | nfal 1556 |
. . . . . . . . 9
⊢
Ⅎ𝑥∀𝑦Ⅎ𝑥𝜓 |
21 | | sp 1491 |
. . . . . . . . 9
⊢
(∀𝑦Ⅎ𝑥𝜓 → Ⅎ𝑥𝜓) |
22 | 20, 21 | nfim1 1551 |
. . . . . . . 8
⊢
Ⅎ𝑥(∀𝑦Ⅎ𝑥𝜓 → 𝜓) |
23 | 18, 22 | nfim 1552 |
. . . . . . 7
⊢
Ⅎ𝑥(𝑦 = 𝑧 → (∀𝑦Ⅎ𝑥𝜓 → 𝜓)) |
24 | 23 | nfal 1556 |
. . . . . 6
⊢
Ⅎ𝑥∀𝑦(𝑦 = 𝑧 → (∀𝑦Ⅎ𝑥𝜓 → 𝜓)) |
25 | 17, 24 | nfxfr 1454 |
. . . . 5
⊢
Ⅎ𝑥(∀𝑦Ⅎ𝑥𝜓 → [𝑧 / 𝑦]𝜓) |
26 | | pm5.5 241 |
. . . . . 6
⊢
(∀𝑦Ⅎ𝑥𝜓 → ((∀𝑦Ⅎ𝑥𝜓 → [𝑧 / 𝑦]𝜓) ↔ [𝑧 / 𝑦]𝜓)) |
27 | 20, 26 | nfbidf 1519 |
. . . . 5
⊢
(∀𝑦Ⅎ𝑥𝜓 → (Ⅎ𝑥(∀𝑦Ⅎ𝑥𝜓 → [𝑧 / 𝑦]𝜓) ↔ Ⅎ𝑥[𝑧 / 𝑦]𝜓)) |
28 | 25, 27 | mpbii 147 |
. . . 4
⊢
(∀𝑦Ⅎ𝑥𝜓 → Ⅎ𝑥[𝑧 / 𝑦]𝜓) |
29 | 5, 28 | syl 14 |
. . 3
⊢ (𝜑 → Ⅎ𝑥[𝑧 / 𝑦]𝜓) |
30 | 2, 29 | nfxfrd 1455 |
. 2
⊢ (𝜑 → Ⅎ𝑥 𝑧 ∈ {𝑦 ∣ 𝜓}) |
31 | 1, 30 | nfcd 2294 |
1
⊢ (𝜑 → Ⅎ𝑥{𝑦 ∣ 𝜓}) |