Step | Hyp | Ref
| Expression |
1 | | axrep2 5211 |
. 2
⊢
∃𝑥(∃𝑦∀𝑤([𝑤 / 𝑧]𝜑 → 𝑤 = 𝑦) → ∀𝑤(𝑤 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑧]𝜑))) |
2 | | nfnae 2434 |
. . 3
⊢
Ⅎ𝑥 ¬
∀𝑦 𝑦 = 𝑧 |
3 | | nfnae 2434 |
. . . . 5
⊢
Ⅎ𝑦 ¬
∀𝑦 𝑦 = 𝑧 |
4 | | nfnae 2434 |
. . . . . 6
⊢
Ⅎ𝑧 ¬
∀𝑦 𝑦 = 𝑧 |
5 | | nfs1v 2153 |
. . . . . . . 8
⊢
Ⅎ𝑧[𝑤 / 𝑧]𝜑 |
6 | 5 | a1i 11 |
. . . . . . 7
⊢ (¬
∀𝑦 𝑦 = 𝑧 → Ⅎ𝑧[𝑤 / 𝑧]𝜑) |
7 | | nfcvd 2908 |
. . . . . . . 8
⊢ (¬
∀𝑦 𝑦 = 𝑧 → Ⅎ𝑧𝑤) |
8 | | nfcvf2 2937 |
. . . . . . . 8
⊢ (¬
∀𝑦 𝑦 = 𝑧 → Ⅎ𝑧𝑦) |
9 | 7, 8 | nfeqd 2917 |
. . . . . . 7
⊢ (¬
∀𝑦 𝑦 = 𝑧 → Ⅎ𝑧 𝑤 = 𝑦) |
10 | 6, 9 | nfimd 1897 |
. . . . . 6
⊢ (¬
∀𝑦 𝑦 = 𝑧 → Ⅎ𝑧([𝑤 / 𝑧]𝜑 → 𝑤 = 𝑦)) |
11 | | sbequ12r 2245 |
. . . . . . . 8
⊢ (𝑤 = 𝑧 → ([𝑤 / 𝑧]𝜑 ↔ 𝜑)) |
12 | | equequ1 2028 |
. . . . . . . 8
⊢ (𝑤 = 𝑧 → (𝑤 = 𝑦 ↔ 𝑧 = 𝑦)) |
13 | 11, 12 | imbi12d 345 |
. . . . . . 7
⊢ (𝑤 = 𝑧 → (([𝑤 / 𝑧]𝜑 → 𝑤 = 𝑦) ↔ (𝜑 → 𝑧 = 𝑦))) |
14 | 13 | a1i 11 |
. . . . . 6
⊢ (¬
∀𝑦 𝑦 = 𝑧 → (𝑤 = 𝑧 → (([𝑤 / 𝑧]𝜑 → 𝑤 = 𝑦) ↔ (𝜑 → 𝑧 = 𝑦)))) |
15 | 4, 10, 14 | cbvald 2407 |
. . . . 5
⊢ (¬
∀𝑦 𝑦 = 𝑧 → (∀𝑤([𝑤 / 𝑧]𝜑 → 𝑤 = 𝑦) ↔ ∀𝑧(𝜑 → 𝑧 = 𝑦))) |
16 | 3, 15 | exbid 2216 |
. . . 4
⊢ (¬
∀𝑦 𝑦 = 𝑧 → (∃𝑦∀𝑤([𝑤 / 𝑧]𝜑 → 𝑤 = 𝑦) ↔ ∃𝑦∀𝑧(𝜑 → 𝑧 = 𝑦))) |
17 | | nfvd 1918 |
. . . . . 6
⊢ (¬
∀𝑦 𝑦 = 𝑧 → Ⅎ𝑧 𝑤 ∈ 𝑥) |
18 | 8 | nfcrd 2896 |
. . . . . . . 8
⊢ (¬
∀𝑦 𝑦 = 𝑧 → Ⅎ𝑧 𝑥 ∈ 𝑦) |
19 | 3, 6 | nfald 2322 |
. . . . . . . 8
⊢ (¬
∀𝑦 𝑦 = 𝑧 → Ⅎ𝑧∀𝑦[𝑤 / 𝑧]𝜑) |
20 | 18, 19 | nfand 1900 |
. . . . . . 7
⊢ (¬
∀𝑦 𝑦 = 𝑧 → Ⅎ𝑧(𝑥 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑧]𝜑)) |
21 | 2, 20 | nfexd 2323 |
. . . . . 6
⊢ (¬
∀𝑦 𝑦 = 𝑧 → Ⅎ𝑧∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑧]𝜑)) |
22 | 17, 21 | nfbid 1905 |
. . . . 5
⊢ (¬
∀𝑦 𝑦 = 𝑧 → Ⅎ𝑧(𝑤 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑧]𝜑))) |
23 | | elequ1 2113 |
. . . . . . . 8
⊢ (𝑤 = 𝑧 → (𝑤 ∈ 𝑥 ↔ 𝑧 ∈ 𝑥)) |
24 | 23 | adantl 482 |
. . . . . . 7
⊢ ((¬
∀𝑦 𝑦 = 𝑧 ∧ 𝑤 = 𝑧) → (𝑤 ∈ 𝑥 ↔ 𝑧 ∈ 𝑥)) |
25 | | nfeqf2 2377 |
. . . . . . . . . . 11
⊢ (¬
∀𝑦 𝑦 = 𝑧 → Ⅎ𝑦 𝑤 = 𝑧) |
26 | 3, 25 | nfan1 2193 |
. . . . . . . . . 10
⊢
Ⅎ𝑦(¬
∀𝑦 𝑦 = 𝑧 ∧ 𝑤 = 𝑧) |
27 | 11 | adantl 482 |
. . . . . . . . . 10
⊢ ((¬
∀𝑦 𝑦 = 𝑧 ∧ 𝑤 = 𝑧) → ([𝑤 / 𝑧]𝜑 ↔ 𝜑)) |
28 | 26, 27 | albid 2215 |
. . . . . . . . 9
⊢ ((¬
∀𝑦 𝑦 = 𝑧 ∧ 𝑤 = 𝑧) → (∀𝑦[𝑤 / 𝑧]𝜑 ↔ ∀𝑦𝜑)) |
29 | 28 | anbi2d 629 |
. . . . . . . 8
⊢ ((¬
∀𝑦 𝑦 = 𝑧 ∧ 𝑤 = 𝑧) → ((𝑥 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑧]𝜑) ↔ (𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑))) |
30 | 29 | exbidv 1924 |
. . . . . . 7
⊢ ((¬
∀𝑦 𝑦 = 𝑧 ∧ 𝑤 = 𝑧) → (∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑧]𝜑) ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑))) |
31 | 24, 30 | bibi12d 346 |
. . . . . 6
⊢ ((¬
∀𝑦 𝑦 = 𝑧 ∧ 𝑤 = 𝑧) → ((𝑤 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑧]𝜑)) ↔ (𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑)))) |
32 | 31 | ex 413 |
. . . . 5
⊢ (¬
∀𝑦 𝑦 = 𝑧 → (𝑤 = 𝑧 → ((𝑤 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑧]𝜑)) ↔ (𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑))))) |
33 | 4, 22, 32 | cbvald 2407 |
. . . 4
⊢ (¬
∀𝑦 𝑦 = 𝑧 → (∀𝑤(𝑤 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑧]𝜑)) ↔ ∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑)))) |
34 | 16, 33 | imbi12d 345 |
. . 3
⊢ (¬
∀𝑦 𝑦 = 𝑧 → ((∃𝑦∀𝑤([𝑤 / 𝑧]𝜑 → 𝑤 = 𝑦) → ∀𝑤(𝑤 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑧]𝜑))) ↔ (∃𝑦∀𝑧(𝜑 → 𝑧 = 𝑦) → ∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑))))) |
35 | 2, 34 | exbid 2216 |
. 2
⊢ (¬
∀𝑦 𝑦 = 𝑧 → (∃𝑥(∃𝑦∀𝑤([𝑤 / 𝑧]𝜑 → 𝑤 = 𝑦) → ∀𝑤(𝑤 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑧]𝜑))) ↔ ∃𝑥(∃𝑦∀𝑧(𝜑 → 𝑧 = 𝑦) → ∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑))))) |
36 | 1, 35 | mpbii 232 |
1
⊢ (¬
∀𝑦 𝑦 = 𝑧 → ∃𝑥(∃𝑦∀𝑧(𝜑 → 𝑧 = 𝑦) → ∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑)))) |