Step | Hyp | Ref
| Expression |
1 | | excom 1741 |
. . . 4
⊢ (∃z∃w∃x∃y(v = ⟨w, z⟩ ∧ (w = ⟨x, y⟩ ∧ φ)) ↔ ∃w∃z∃x∃y(v = ⟨w, z⟩ ∧ (w = ⟨x, y⟩ ∧ φ))) |
2 | | exrot4 1745 |
. . . . 5
⊢ (∃z∃w∃x∃y(v = ⟨w, z⟩ ∧ (w = ⟨x, y⟩ ∧ φ)) ↔ ∃x∃y∃z∃w(v = ⟨w, z⟩ ∧ (w = ⟨x, y⟩ ∧ φ))) |
3 | | an12 772 |
. . . . . . . 8
⊢ ((v = ⟨w, z⟩ ∧ (w = ⟨x, y⟩ ∧ φ)) ↔ (w = ⟨x, y⟩ ∧ (v = ⟨w, z⟩ ∧ φ))) |
4 | 3 | exbii 1582 |
. . . . . . 7
⊢ (∃w(v = ⟨w, z⟩ ∧ (w = ⟨x, y⟩ ∧ φ)) ↔ ∃w(w = ⟨x, y⟩ ∧ (v = ⟨w, z⟩ ∧ φ))) |
5 | | vex 2863 |
. . . . . . . . 9
⊢ x ∈
V |
6 | | vex 2863 |
. . . . . . . . 9
⊢ y ∈
V |
7 | 5, 6 | opex 4589 |
. . . . . . . 8
⊢ ⟨x, y⟩ ∈ V |
8 | | opeq1 4579 |
. . . . . . . . . 10
⊢ (w = ⟨x, y⟩ → ⟨w, z⟩ = ⟨⟨x, y⟩, z⟩) |
9 | 8 | eqeq2d 2364 |
. . . . . . . . 9
⊢ (w = ⟨x, y⟩ → (v =
⟨w,
z⟩ ↔
v = ⟨⟨x, y⟩, z⟩)) |
10 | 9 | anbi1d 685 |
. . . . . . . 8
⊢ (w = ⟨x, y⟩ → ((v =
⟨w,
z⟩ ∧ φ) ↔
(v = ⟨⟨x, y⟩, z⟩ ∧ φ))) |
11 | 7, 10 | ceqsexv 2895 |
. . . . . . 7
⊢ (∃w(w = ⟨x, y⟩ ∧ (v = ⟨w, z⟩ ∧ φ)) ↔ (v = ⟨⟨x, y⟩, z⟩ ∧ φ)) |
12 | 4, 11 | bitri 240 |
. . . . . 6
⊢ (∃w(v = ⟨w, z⟩ ∧ (w = ⟨x, y⟩ ∧ φ)) ↔ (v = ⟨⟨x, y⟩, z⟩ ∧ φ)) |
13 | 12 | 3exbii 1584 |
. . . . 5
⊢ (∃x∃y∃z∃w(v = ⟨w, z⟩ ∧ (w = ⟨x, y⟩ ∧ φ)) ↔ ∃x∃y∃z(v = ⟨⟨x, y⟩, z⟩ ∧ φ)) |
14 | 2, 13 | bitri 240 |
. . . 4
⊢ (∃z∃w∃x∃y(v = ⟨w, z⟩ ∧ (w = ⟨x, y⟩ ∧ φ)) ↔ ∃x∃y∃z(v = ⟨⟨x, y⟩, z⟩ ∧ φ)) |
15 | | 19.42vv 1907 |
. . . . 5
⊢ (∃x∃y(v = ⟨w, z⟩ ∧ (w = ⟨x, y⟩ ∧ φ)) ↔ (v = ⟨w, z⟩ ∧ ∃x∃y(w = ⟨x, y⟩ ∧ φ))) |
16 | 15 | 2exbii 1583 |
. . . 4
⊢ (∃w∃z∃x∃y(v = ⟨w, z⟩ ∧ (w = ⟨x, y⟩ ∧ φ)) ↔ ∃w∃z(v = ⟨w, z⟩ ∧ ∃x∃y(w = ⟨x, y⟩ ∧ φ))) |
17 | 1, 14, 16 | 3bitr3i 266 |
. . 3
⊢ (∃x∃y∃z(v = ⟨⟨x, y⟩, z⟩ ∧ φ) ↔
∃w∃z(v = ⟨w, z⟩ ∧ ∃x∃y(w = ⟨x, y⟩ ∧ φ))) |
18 | 17 | abbii 2466 |
. 2
⊢ {v ∣ ∃x∃y∃z(v = ⟨⟨x, y⟩, z⟩ ∧ φ)} =
{v ∣
∃w∃z(v = ⟨w, z⟩ ∧ ∃x∃y(w = ⟨x, y⟩ ∧ φ))} |
19 | | df-oprab 5529 |
. 2
⊢ {⟨⟨x, y⟩, z⟩ ∣ φ} = {v
∣ ∃x∃y∃z(v = ⟨⟨x, y⟩, z⟩ ∧ φ)} |
20 | | df-opab 4624 |
. 2
⊢ {⟨w, z⟩ ∣ ∃x∃y(w = ⟨x, y⟩ ∧ φ)} =
{v ∣
∃w∃z(v = ⟨w, z⟩ ∧ ∃x∃y(w = ⟨x, y⟩ ∧ φ))} |
21 | 18, 19, 20 | 3eqtr4i 2383 |
1
⊢ {⟨⟨x, y⟩, z⟩ ∣ φ} = {⟨w, z⟩ ∣ ∃x∃y(w = ⟨x, y⟩ ∧ φ)} |