Step | Hyp | Ref
| Expression |
1 | | excom 1551 |
. . . 4
⊢ (∃z∃w∃x∃y(v = 〈w,
z〉 ∧
(w = 〈x, y〉 ∧ φ)) ↔
∃w∃z∃x∃y(v = 〈w,
z〉 ∧
(w = 〈x, y〉 ∧ φ))) |
2 | | exrot4 1578 |
. . . . 5
⊢ (∃z∃w∃x∃y(v = 〈w,
z〉 ∧
(w = 〈x, y〉 ∧ φ)) ↔
∃x∃y∃z∃w(v = 〈w,
z〉 ∧
(w = 〈x, y〉 ∧ φ))) |
3 | | opeq1 3540 |
. . . . . . . . . . . 12
⊢ (w = 〈x,
y〉 → 〈w, z〉 =
〈〈x, y〉, z〉) |
4 | 3 | eqeq2d 2048 |
. . . . . . . . . . 11
⊢ (w = 〈x,
y〉 → (v = 〈w,
z〉 ↔ v = 〈〈x, y〉,
z〉)) |
5 | 4 | pm5.32ri 428 |
. . . . . . . . . 10
⊢
((v = 〈w, z〉 ∧ w =
〈x, y〉) ↔ (v = 〈〈x, y〉,
z〉 ∧
w = 〈x, y〉)) |
6 | 5 | anbi1i 431 |
. . . . . . . . 9
⊢
(((v = 〈w, z〉 ∧ w =
〈x, y〉) ∧ φ) ↔ ((v = 〈〈x, y〉,
z〉 ∧
w = 〈x, y〉)
∧ φ)) |
7 | | anass 381 |
. . . . . . . . 9
⊢
(((v = 〈w, z〉 ∧ w =
〈x, y〉) ∧ φ) ↔ (v = 〈w,
z〉 ∧
(w = 〈x, y〉 ∧ φ))) |
8 | | an32 496 |
. . . . . . . . 9
⊢
(((v = 〈〈x, y〉,
z〉 ∧
w = 〈x, y〉)
∧ φ)
↔ ((v = 〈〈x, y〉,
z〉 ∧
φ) ∧
w = 〈x, y〉)) |
9 | 6, 7, 8 | 3bitr3i 199 |
. . . . . . . 8
⊢
((v = 〈w, z〉 ∧ (w =
〈x, y〉 ∧ φ)) ↔ ((v = 〈〈x, y〉,
z〉 ∧
φ) ∧
w = 〈x, y〉)) |
10 | 9 | exbii 1493 |
. . . . . . 7
⊢ (∃w(v = 〈w,
z〉 ∧
(w = 〈x, y〉 ∧ φ)) ↔
∃w((v =
〈〈x, y〉, z〉
∧ φ)
∧ w =
〈x, y〉)) |
11 | | vex 2554 |
. . . . . . . . . 10
⊢ x ∈
V |
12 | | vex 2554 |
. . . . . . . . . 10
⊢ y ∈
V |
13 | 11, 12 | opex 3957 |
. . . . . . . . 9
⊢
〈x, y〉 ∈
V |
14 | 13 | isseti 2557 |
. . . . . . . 8
⊢ ∃w w = 〈x,
y〉 |
15 | | 19.42v 1783 |
. . . . . . . 8
⊢ (∃w((v = 〈〈x, y〉,
z〉 ∧
φ) ∧
w = 〈x, y〉)
↔ ((v = 〈〈x, y〉,
z〉 ∧
φ) ∧
∃w
w = 〈x, y〉)) |
16 | 14, 15 | mpbiran2 847 |
. . . . . . 7
⊢ (∃w((v = 〈〈x, y〉,
z〉 ∧
φ) ∧
w = 〈x, y〉)
↔ (v = 〈〈x, y〉,
z〉 ∧
φ)) |
17 | 10, 16 | bitri 173 |
. . . . . 6
⊢ (∃w(v = 〈w,
z〉 ∧
(w = 〈x, y〉 ∧ φ)) ↔
(v = 〈〈x, y〉,
z〉 ∧
φ)) |
18 | 17 | 3exbii 1495 |
. . . . 5
⊢ (∃x∃y∃z∃w(v = 〈w,
z〉 ∧
(w = 〈x, y〉 ∧ φ)) ↔
∃x∃y∃z(v = 〈〈x, y〉,
z〉 ∧
φ)) |
19 | 2, 18 | bitri 173 |
. . . 4
⊢ (∃z∃w∃x∃y(v = 〈w,
z〉 ∧
(w = 〈x, y〉 ∧ φ)) ↔
∃x∃y∃z(v = 〈〈x, y〉,
z〉 ∧
φ)) |
20 | | 19.42vv 1785 |
. . . . 5
⊢ (∃x∃y(v = 〈w,
z〉 ∧
(w = 〈x, y〉 ∧ φ)) ↔
(v = 〈w, z〉 ∧ ∃x∃y(w =
〈x, y〉 ∧ φ))) |
21 | 20 | 2exbii 1494 |
. . . 4
⊢ (∃w∃z∃x∃y(v = 〈w,
z〉 ∧
(w = 〈x, y〉 ∧ φ)) ↔
∃w∃z(v = 〈w,
z〉 ∧
∃x∃y(w = 〈x,
y〉 ∧
φ))) |
22 | 1, 19, 21 | 3bitr3i 199 |
. . 3
⊢ (∃x∃y∃z(v = 〈〈x, y〉,
z〉 ∧
φ) ↔ ∃w∃z(v = 〈w,
z〉 ∧
∃x∃y(w = 〈x,
y〉 ∧
φ))) |
23 | 22 | abbii 2150 |
. 2
⊢ {v ∣ ∃x∃y∃z(v = 〈〈x, y〉,
z〉 ∧
φ)} = {v ∣ ∃w∃z(v = 〈w,
z〉 ∧
∃x∃y(w = 〈x,
y〉 ∧
φ))} |
24 | | df-oprab 5459 |
. 2
⊢
{〈〈x, y〉, z〉
∣ φ} = {v ∣ ∃x∃y∃z(v = 〈〈x, y〉,
z〉 ∧
φ)} |
25 | | df-opab 3810 |
. 2
⊢
{〈w, z〉 ∣ ∃x∃y(w = 〈x,
y〉 ∧
φ)} = {v ∣ ∃w∃z(v = 〈w,
z〉 ∧
∃x∃y(w = 〈x,
y〉 ∧
φ))} |
26 | 23, 24, 25 | 3eqtr4i 2067 |
1
⊢
{〈〈x, y〉, z〉
∣ φ} = {〈w, z〉
∣ ∃x∃y(w =
〈x, y〉 ∧ φ)} |