Step | Hyp | Ref
| Expression |
1 | | axrep2 4773 |
. 2
⊢
∃𝑥(∃𝑦∀𝑤([𝑤 / 𝑧]𝜑 → 𝑤 = 𝑦) → ∀𝑤(𝑤 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑧]𝜑))) |
2 | | nfnae 2318 |
. . 3
⊢
Ⅎ𝑥 ¬
∀𝑦 𝑦 = 𝑧 |
3 | | nfnae 2318 |
. . . . 5
⊢
Ⅎ𝑦 ¬
∀𝑦 𝑦 = 𝑧 |
4 | | nfnae 2318 |
. . . . . 6
⊢
Ⅎ𝑧 ¬
∀𝑦 𝑦 = 𝑧 |
5 | | nfs1v 2437 |
. . . . . . . 8
⊢
Ⅎ𝑧[𝑤 / 𝑧]𝜑 |
6 | 5 | a1i 11 |
. . . . . . 7
⊢ (¬
∀𝑦 𝑦 = 𝑧 → Ⅎ𝑧[𝑤 / 𝑧]𝜑) |
7 | | nfcvd 2765 |
. . . . . . . 8
⊢ (¬
∀𝑦 𝑦 = 𝑧 → Ⅎ𝑧𝑤) |
8 | | nfcvf2 2789 |
. . . . . . . 8
⊢ (¬
∀𝑦 𝑦 = 𝑧 → Ⅎ𝑧𝑦) |
9 | 7, 8 | nfeqd 2772 |
. . . . . . 7
⊢ (¬
∀𝑦 𝑦 = 𝑧 → Ⅎ𝑧 𝑤 = 𝑦) |
10 | 6, 9 | nfimd 1823 |
. . . . . 6
⊢ (¬
∀𝑦 𝑦 = 𝑧 → Ⅎ𝑧([𝑤 / 𝑧]𝜑 → 𝑤 = 𝑦)) |
11 | | sbequ12r 2112 |
. . . . . . . 8
⊢ (𝑤 = 𝑧 → ([𝑤 / 𝑧]𝜑 ↔ 𝜑)) |
12 | | equequ1 1952 |
. . . . . . . 8
⊢ (𝑤 = 𝑧 → (𝑤 = 𝑦 ↔ 𝑧 = 𝑦)) |
13 | 11, 12 | imbi12d 334 |
. . . . . . 7
⊢ (𝑤 = 𝑧 → (([𝑤 / 𝑧]𝜑 → 𝑤 = 𝑦) ↔ (𝜑 → 𝑧 = 𝑦))) |
14 | 13 | a1i 11 |
. . . . . 6
⊢ (¬
∀𝑦 𝑦 = 𝑧 → (𝑤 = 𝑧 → (([𝑤 / 𝑧]𝜑 → 𝑤 = 𝑦) ↔ (𝜑 → 𝑧 = 𝑦)))) |
15 | 4, 10, 14 | cbvald 2277 |
. . . . 5
⊢ (¬
∀𝑦 𝑦 = 𝑧 → (∀𝑤([𝑤 / 𝑧]𝜑 → 𝑤 = 𝑦) ↔ ∀𝑧(𝜑 → 𝑧 = 𝑦))) |
16 | 3, 15 | exbid 2091 |
. . . 4
⊢ (¬
∀𝑦 𝑦 = 𝑧 → (∃𝑦∀𝑤([𝑤 / 𝑧]𝜑 → 𝑤 = 𝑦) ↔ ∃𝑦∀𝑧(𝜑 → 𝑧 = 𝑦))) |
17 | | nfvd 1844 |
. . . . . 6
⊢ (¬
∀𝑦 𝑦 = 𝑧 → Ⅎ𝑧 𝑤 ∈ 𝑥) |
18 | 8 | nfcrd 2771 |
. . . . . . . 8
⊢ (¬
∀𝑦 𝑦 = 𝑧 → Ⅎ𝑧 𝑥 ∈ 𝑦) |
19 | 3, 6 | nfald 2165 |
. . . . . . . 8
⊢ (¬
∀𝑦 𝑦 = 𝑧 → Ⅎ𝑧∀𝑦[𝑤 / 𝑧]𝜑) |
20 | 18, 19 | nfand 1826 |
. . . . . . 7
⊢ (¬
∀𝑦 𝑦 = 𝑧 → Ⅎ𝑧(𝑥 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑧]𝜑)) |
21 | 2, 20 | nfexd 2167 |
. . . . . 6
⊢ (¬
∀𝑦 𝑦 = 𝑧 → Ⅎ𝑧∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑧]𝜑)) |
22 | 17, 21 | nfbid 1832 |
. . . . 5
⊢ (¬
∀𝑦 𝑦 = 𝑧 → Ⅎ𝑧(𝑤 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑧]𝜑))) |
23 | | elequ1 1997 |
. . . . . . . 8
⊢ (𝑤 = 𝑧 → (𝑤 ∈ 𝑥 ↔ 𝑧 ∈ 𝑥)) |
24 | 23 | adantl 482 |
. . . . . . 7
⊢ ((¬
∀𝑦 𝑦 = 𝑧 ∧ 𝑤 = 𝑧) → (𝑤 ∈ 𝑥 ↔ 𝑧 ∈ 𝑥)) |
25 | | nfeqf2 2297 |
. . . . . . . . . . 11
⊢ (¬
∀𝑦 𝑦 = 𝑧 → Ⅎ𝑦 𝑤 = 𝑧) |
26 | 3, 25 | nfan1 2068 |
. . . . . . . . . 10
⊢
Ⅎ𝑦(¬
∀𝑦 𝑦 = 𝑧 ∧ 𝑤 = 𝑧) |
27 | 11 | adantl 482 |
. . . . . . . . . 10
⊢ ((¬
∀𝑦 𝑦 = 𝑧 ∧ 𝑤 = 𝑧) → ([𝑤 / 𝑧]𝜑 ↔ 𝜑)) |
28 | 26, 27 | albid 2090 |
. . . . . . . . 9
⊢ ((¬
∀𝑦 𝑦 = 𝑧 ∧ 𝑤 = 𝑧) → (∀𝑦[𝑤 / 𝑧]𝜑 ↔ ∀𝑦𝜑)) |
29 | 28 | anbi2d 740 |
. . . . . . . 8
⊢ ((¬
∀𝑦 𝑦 = 𝑧 ∧ 𝑤 = 𝑧) → ((𝑥 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑧]𝜑) ↔ (𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑))) |
30 | 29 | exbidv 1850 |
. . . . . . 7
⊢ ((¬
∀𝑦 𝑦 = 𝑧 ∧ 𝑤 = 𝑧) → (∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑧]𝜑) ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑))) |
31 | 24, 30 | bibi12d 335 |
. . . . . 6
⊢ ((¬
∀𝑦 𝑦 = 𝑧 ∧ 𝑤 = 𝑧) → ((𝑤 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑧]𝜑)) ↔ (𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑)))) |
32 | 31 | ex 450 |
. . . . 5
⊢ (¬
∀𝑦 𝑦 = 𝑧 → (𝑤 = 𝑧 → ((𝑤 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑧]𝜑)) ↔ (𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑))))) |
33 | 4, 22, 32 | cbvald 2277 |
. . . 4
⊢ (¬
∀𝑦 𝑦 = 𝑧 → (∀𝑤(𝑤 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑧]𝜑)) ↔ ∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑)))) |
34 | 16, 33 | imbi12d 334 |
. . 3
⊢ (¬
∀𝑦 𝑦 = 𝑧 → ((∃𝑦∀𝑤([𝑤 / 𝑧]𝜑 → 𝑤 = 𝑦) → ∀𝑤(𝑤 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑧]𝜑))) ↔ (∃𝑦∀𝑧(𝜑 → 𝑧 = 𝑦) → ∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑))))) |
35 | 2, 34 | exbid 2091 |
. 2
⊢ (¬
∀𝑦 𝑦 = 𝑧 → (∃𝑥(∃𝑦∀𝑤([𝑤 / 𝑧]𝜑 → 𝑤 = 𝑦) → ∀𝑤(𝑤 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑧]𝜑))) ↔ ∃𝑥(∃𝑦∀𝑧(𝜑 → 𝑧 = 𝑦) → ∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑))))) |
36 | 1, 35 | mpbii 223 |
1
⊢ (¬
∀𝑦 𝑦 = 𝑧 → ∃𝑥(∃𝑦∀𝑧(𝜑 → 𝑧 = 𝑦) → ∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑)))) |