Step | Hyp | Ref
| Expression |
1 | | elequ2 2121 |
. . . . . . . . 9
⊢ (𝑤 = 𝑦 → (𝑥 ∈ 𝑤 ↔ 𝑥 ∈ 𝑦)) |
2 | 1 | anbi1d 630 |
. . . . . . . 8
⊢ (𝑤 = 𝑦 → ((𝑥 ∈ 𝑤 ∧ 𝜑) ↔ (𝑥 ∈ 𝑦 ∧ 𝜑))) |
3 | 2 | exbidv 1924 |
. . . . . . 7
⊢ (𝑤 = 𝑦 → (∃𝑥(𝑥 ∈ 𝑤 ∧ 𝜑) ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ 𝜑))) |
4 | 3 | bibi2d 343 |
. . . . . 6
⊢ (𝑤 = 𝑦 → ((𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑤 ∧ 𝜑)) ↔ (𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ 𝜑)))) |
5 | 4 | albidv 1923 |
. . . . 5
⊢ (𝑤 = 𝑦 → (∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑤 ∧ 𝜑)) ↔ ∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ 𝜑)))) |
6 | 5 | exbidv 1924 |
. . . 4
⊢ (𝑤 = 𝑦 → (∃𝑥∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑤 ∧ 𝜑)) ↔ ∃𝑥∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ 𝜑)))) |
7 | 6 | imbi2d 341 |
. . 3
⊢ (𝑤 = 𝑦 → ((∀𝑥∃𝑦∀𝑧(𝜑 → 𝑧 = 𝑦) → ∃𝑥∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑤 ∧ 𝜑))) ↔ (∀𝑥∃𝑦∀𝑧(𝜑 → 𝑧 = 𝑦) → ∃𝑥∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ 𝜑))))) |
8 | | ax-rep 5209 |
. . . 4
⊢
(∀𝑥∃𝑦∀𝑧(∀𝑦𝜑 → 𝑧 = 𝑦) → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ ∃𝑥(𝑥 ∈ 𝑤 ∧ ∀𝑦𝜑))) |
9 | | 19.3v 1985 |
. . . . . . . 8
⊢
(∀𝑦𝜑 ↔ 𝜑) |
10 | 9 | imbi1i 350 |
. . . . . . 7
⊢
((∀𝑦𝜑 → 𝑧 = 𝑦) ↔ (𝜑 → 𝑧 = 𝑦)) |
11 | 10 | albii 1822 |
. . . . . 6
⊢
(∀𝑧(∀𝑦𝜑 → 𝑧 = 𝑦) ↔ ∀𝑧(𝜑 → 𝑧 = 𝑦)) |
12 | 11 | exbii 1850 |
. . . . 5
⊢
(∃𝑦∀𝑧(∀𝑦𝜑 → 𝑧 = 𝑦) ↔ ∃𝑦∀𝑧(𝜑 → 𝑧 = 𝑦)) |
13 | 12 | albii 1822 |
. . . 4
⊢
(∀𝑥∃𝑦∀𝑧(∀𝑦𝜑 → 𝑧 = 𝑦) ↔ ∀𝑥∃𝑦∀𝑧(𝜑 → 𝑧 = 𝑦)) |
14 | | nfv 1917 |
. . . . . . 7
⊢
Ⅎ𝑥 𝑧 ∈ 𝑦 |
15 | | nfe1 2147 |
. . . . . . 7
⊢
Ⅎ𝑥∃𝑥(𝑥 ∈ 𝑤 ∧ ∀𝑦𝜑) |
16 | 14, 15 | nfbi 1906 |
. . . . . 6
⊢
Ⅎ𝑥(𝑧 ∈ 𝑦 ↔ ∃𝑥(𝑥 ∈ 𝑤 ∧ ∀𝑦𝜑)) |
17 | 16 | nfal 2317 |
. . . . 5
⊢
Ⅎ𝑥∀𝑧(𝑧 ∈ 𝑦 ↔ ∃𝑥(𝑥 ∈ 𝑤 ∧ ∀𝑦𝜑)) |
18 | | nfv 1917 |
. . . . 5
⊢
Ⅎ𝑦∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑤 ∧ 𝜑)) |
19 | | elequ2 2121 |
. . . . . . 7
⊢ (𝑦 = 𝑥 → (𝑧 ∈ 𝑦 ↔ 𝑧 ∈ 𝑥)) |
20 | 9 | anbi2i 623 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝑤 ∧ ∀𝑦𝜑) ↔ (𝑥 ∈ 𝑤 ∧ 𝜑)) |
21 | 20 | exbii 1850 |
. . . . . . . 8
⊢
(∃𝑥(𝑥 ∈ 𝑤 ∧ ∀𝑦𝜑) ↔ ∃𝑥(𝑥 ∈ 𝑤 ∧ 𝜑)) |
22 | 21 | a1i 11 |
. . . . . . 7
⊢ (𝑦 = 𝑥 → (∃𝑥(𝑥 ∈ 𝑤 ∧ ∀𝑦𝜑) ↔ ∃𝑥(𝑥 ∈ 𝑤 ∧ 𝜑))) |
23 | 19, 22 | bibi12d 346 |
. . . . . 6
⊢ (𝑦 = 𝑥 → ((𝑧 ∈ 𝑦 ↔ ∃𝑥(𝑥 ∈ 𝑤 ∧ ∀𝑦𝜑)) ↔ (𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑤 ∧ 𝜑)))) |
24 | 23 | albidv 1923 |
. . . . 5
⊢ (𝑦 = 𝑥 → (∀𝑧(𝑧 ∈ 𝑦 ↔ ∃𝑥(𝑥 ∈ 𝑤 ∧ ∀𝑦𝜑)) ↔ ∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑤 ∧ 𝜑)))) |
25 | 17, 18, 24 | cbvexv1 2339 |
. . . 4
⊢
(∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ ∃𝑥(𝑥 ∈ 𝑤 ∧ ∀𝑦𝜑)) ↔ ∃𝑥∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑤 ∧ 𝜑))) |
26 | 8, 13, 25 | 3imtr3i 291 |
. . 3
⊢
(∀𝑥∃𝑦∀𝑧(𝜑 → 𝑧 = 𝑦) → ∃𝑥∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑤 ∧ 𝜑))) |
27 | 7, 26 | chvarvv 2002 |
. 2
⊢
(∀𝑥∃𝑦∀𝑧(𝜑 → 𝑧 = 𝑦) → ∃𝑥∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ 𝜑))) |
28 | 27 | 19.35ri 1882 |
1
⊢
∃𝑥(∃𝑦∀𝑧(𝜑 → 𝑧 = 𝑦) → ∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ 𝜑))) |