Step | Hyp | Ref
| Expression |
1 | | nfv 1830 |
. . . 4
⊢
Ⅎ𝑦(𝑤 = 𝑥 ∧ 𝜑) |
2 | 1 | bj-axrep5 31980 |
. . 3
⊢
(∀𝑤(𝑤 ∈ 𝑧 → ∃𝑦∀𝑥((𝑤 = 𝑥 ∧ 𝜑) → 𝑥 = 𝑦)) → ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ ∃𝑤(𝑤 ∈ 𝑧 ∧ (𝑤 = 𝑥 ∧ 𝜑)))) |
3 | | equtr 1935 |
. . . . . . . 8
⊢ (𝑦 = 𝑤 → (𝑤 = 𝑥 → 𝑦 = 𝑥)) |
4 | | equcomi 1931 |
. . . . . . . 8
⊢ (𝑦 = 𝑥 → 𝑥 = 𝑦) |
5 | 3, 4 | syl6 34 |
. . . . . . 7
⊢ (𝑦 = 𝑤 → (𝑤 = 𝑥 → 𝑥 = 𝑦)) |
6 | 5 | adantrd 483 |
. . . . . 6
⊢ (𝑦 = 𝑤 → ((𝑤 = 𝑥 ∧ 𝜑) → 𝑥 = 𝑦)) |
7 | 6 | alrimiv 1842 |
. . . . 5
⊢ (𝑦 = 𝑤 → ∀𝑥((𝑤 = 𝑥 ∧ 𝜑) → 𝑥 = 𝑦)) |
8 | 7 | a1d 25 |
. . . 4
⊢ (𝑦 = 𝑤 → (𝑤 ∈ 𝑧 → ∀𝑥((𝑤 = 𝑥 ∧ 𝜑) → 𝑥 = 𝑦))) |
9 | 8 | bj-spimevv 31909 |
. . 3
⊢ (𝑤 ∈ 𝑧 → ∃𝑦∀𝑥((𝑤 = 𝑥 ∧ 𝜑) → 𝑥 = 𝑦)) |
10 | 2, 9 | mpg 1715 |
. 2
⊢
∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ ∃𝑤(𝑤 ∈ 𝑧 ∧ (𝑤 = 𝑥 ∧ 𝜑))) |
11 | | an12 834 |
. . . . . . 7
⊢ ((𝑤 = 𝑥 ∧ (𝑤 ∈ 𝑧 ∧ 𝜑)) ↔ (𝑤 ∈ 𝑧 ∧ (𝑤 = 𝑥 ∧ 𝜑))) |
12 | 11 | exbii 1764 |
. . . . . 6
⊢
(∃𝑤(𝑤 = 𝑥 ∧ (𝑤 ∈ 𝑧 ∧ 𝜑)) ↔ ∃𝑤(𝑤 ∈ 𝑧 ∧ (𝑤 = 𝑥 ∧ 𝜑))) |
13 | | elequ1 1984 |
. . . . . . . 8
⊢ (𝑤 = 𝑥 → (𝑤 ∈ 𝑧 ↔ 𝑥 ∈ 𝑧)) |
14 | 13 | anbi1d 737 |
. . . . . . 7
⊢ (𝑤 = 𝑥 → ((𝑤 ∈ 𝑧 ∧ 𝜑) ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))) |
15 | 14 | equsexvw 1919 |
. . . . . 6
⊢
(∃𝑤(𝑤 = 𝑥 ∧ (𝑤 ∈ 𝑧 ∧ 𝜑)) ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)) |
16 | 12, 15 | bitr3i 265 |
. . . . 5
⊢
(∃𝑤(𝑤 ∈ 𝑧 ∧ (𝑤 = 𝑥 ∧ 𝜑)) ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)) |
17 | 16 | bibi2i 326 |
. . . 4
⊢ ((𝑥 ∈ 𝑦 ↔ ∃𝑤(𝑤 ∈ 𝑧 ∧ (𝑤 = 𝑥 ∧ 𝜑))) ↔ (𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))) |
18 | 17 | albii 1737 |
. . 3
⊢
(∀𝑥(𝑥 ∈ 𝑦 ↔ ∃𝑤(𝑤 ∈ 𝑧 ∧ (𝑤 = 𝑥 ∧ 𝜑))) ↔ ∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))) |
19 | 18 | exbii 1764 |
. 2
⊢
(∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ ∃𝑤(𝑤 ∈ 𝑧 ∧ (𝑤 = 𝑥 ∧ 𝜑))) ↔ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))) |
20 | 10, 19 | mpbi 219 |
1
⊢
∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)) |