Step | Hyp | Ref
| Expression |
1 | | excom 1657 |
. . . 4
⊢
(∃𝑧∃𝑤∃𝑥∃𝑦(𝑣 = 〈𝑤, 𝑧〉 ∧ (𝑤 = 〈𝑥, 𝑦〉 ∧ 𝜑)) ↔ ∃𝑤∃𝑧∃𝑥∃𝑦(𝑣 = 〈𝑤, 𝑧〉 ∧ (𝑤 = 〈𝑥, 𝑦〉 ∧ 𝜑))) |
2 | | exrot4 1684 |
. . . . 5
⊢
(∃𝑧∃𝑤∃𝑥∃𝑦(𝑣 = 〈𝑤, 𝑧〉 ∧ (𝑤 = 〈𝑥, 𝑦〉 ∧ 𝜑)) ↔ ∃𝑥∃𝑦∃𝑧∃𝑤(𝑣 = 〈𝑤, 𝑧〉 ∧ (𝑤 = 〈𝑥, 𝑦〉 ∧ 𝜑))) |
3 | | opeq1 3763 |
. . . . . . . . . . . 12
⊢ (𝑤 = 〈𝑥, 𝑦〉 → 〈𝑤, 𝑧〉 = 〈〈𝑥, 𝑦〉, 𝑧〉) |
4 | 3 | eqeq2d 2182 |
. . . . . . . . . . 11
⊢ (𝑤 = 〈𝑥, 𝑦〉 → (𝑣 = 〈𝑤, 𝑧〉 ↔ 𝑣 = 〈〈𝑥, 𝑦〉, 𝑧〉)) |
5 | 4 | pm5.32ri 452 |
. . . . . . . . . 10
⊢ ((𝑣 = 〈𝑤, 𝑧〉 ∧ 𝑤 = 〈𝑥, 𝑦〉) ↔ (𝑣 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝑤 = 〈𝑥, 𝑦〉)) |
6 | 5 | anbi1i 455 |
. . . . . . . . 9
⊢ (((𝑣 = 〈𝑤, 𝑧〉 ∧ 𝑤 = 〈𝑥, 𝑦〉) ∧ 𝜑) ↔ ((𝑣 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝑤 = 〈𝑥, 𝑦〉) ∧ 𝜑)) |
7 | | anass 399 |
. . . . . . . . 9
⊢ (((𝑣 = 〈𝑤, 𝑧〉 ∧ 𝑤 = 〈𝑥, 𝑦〉) ∧ 𝜑) ↔ (𝑣 = 〈𝑤, 𝑧〉 ∧ (𝑤 = 〈𝑥, 𝑦〉 ∧ 𝜑))) |
8 | | an32 557 |
. . . . . . . . 9
⊢ (((𝑣 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝑤 = 〈𝑥, 𝑦〉) ∧ 𝜑) ↔ ((𝑣 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) ∧ 𝑤 = 〈𝑥, 𝑦〉)) |
9 | 6, 7, 8 | 3bitr3i 209 |
. . . . . . . 8
⊢ ((𝑣 = 〈𝑤, 𝑧〉 ∧ (𝑤 = 〈𝑥, 𝑦〉 ∧ 𝜑)) ↔ ((𝑣 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) ∧ 𝑤 = 〈𝑥, 𝑦〉)) |
10 | 9 | exbii 1598 |
. . . . . . 7
⊢
(∃𝑤(𝑣 = 〈𝑤, 𝑧〉 ∧ (𝑤 = 〈𝑥, 𝑦〉 ∧ 𝜑)) ↔ ∃𝑤((𝑣 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) ∧ 𝑤 = 〈𝑥, 𝑦〉)) |
11 | | vex 2733 |
. . . . . . . . . 10
⊢ 𝑥 ∈ V |
12 | | vex 2733 |
. . . . . . . . . 10
⊢ 𝑦 ∈ V |
13 | 11, 12 | opex 4212 |
. . . . . . . . 9
⊢
〈𝑥, 𝑦〉 ∈ V |
14 | 13 | isseti 2738 |
. . . . . . . 8
⊢
∃𝑤 𝑤 = 〈𝑥, 𝑦〉 |
15 | | 19.42v 1899 |
. . . . . . . 8
⊢
(∃𝑤((𝑣 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) ∧ 𝑤 = 〈𝑥, 𝑦〉) ↔ ((𝑣 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) ∧ ∃𝑤 𝑤 = 〈𝑥, 𝑦〉)) |
16 | 14, 15 | mpbiran2 936 |
. . . . . . 7
⊢
(∃𝑤((𝑣 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) ∧ 𝑤 = 〈𝑥, 𝑦〉) ↔ (𝑣 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑)) |
17 | 10, 16 | bitri 183 |
. . . . . 6
⊢
(∃𝑤(𝑣 = 〈𝑤, 𝑧〉 ∧ (𝑤 = 〈𝑥, 𝑦〉 ∧ 𝜑)) ↔ (𝑣 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑)) |
18 | 17 | 3exbii 1600 |
. . . . 5
⊢
(∃𝑥∃𝑦∃𝑧∃𝑤(𝑣 = 〈𝑤, 𝑧〉 ∧ (𝑤 = 〈𝑥, 𝑦〉 ∧ 𝜑)) ↔ ∃𝑥∃𝑦∃𝑧(𝑣 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑)) |
19 | 2, 18 | bitri 183 |
. . . 4
⊢
(∃𝑧∃𝑤∃𝑥∃𝑦(𝑣 = 〈𝑤, 𝑧〉 ∧ (𝑤 = 〈𝑥, 𝑦〉 ∧ 𝜑)) ↔ ∃𝑥∃𝑦∃𝑧(𝑣 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑)) |
20 | | 19.42vv 1904 |
. . . . 5
⊢
(∃𝑥∃𝑦(𝑣 = 〈𝑤, 𝑧〉 ∧ (𝑤 = 〈𝑥, 𝑦〉 ∧ 𝜑)) ↔ (𝑣 = 〈𝑤, 𝑧〉 ∧ ∃𝑥∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝜑))) |
21 | 20 | 2exbii 1599 |
. . . 4
⊢
(∃𝑤∃𝑧∃𝑥∃𝑦(𝑣 = 〈𝑤, 𝑧〉 ∧ (𝑤 = 〈𝑥, 𝑦〉 ∧ 𝜑)) ↔ ∃𝑤∃𝑧(𝑣 = 〈𝑤, 𝑧〉 ∧ ∃𝑥∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝜑))) |
22 | 1, 19, 21 | 3bitr3i 209 |
. . 3
⊢
(∃𝑥∃𝑦∃𝑧(𝑣 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) ↔ ∃𝑤∃𝑧(𝑣 = 〈𝑤, 𝑧〉 ∧ ∃𝑥∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝜑))) |
23 | 22 | abbii 2286 |
. 2
⊢ {𝑣 ∣ ∃𝑥∃𝑦∃𝑧(𝑣 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑)} = {𝑣 ∣ ∃𝑤∃𝑧(𝑣 = 〈𝑤, 𝑧〉 ∧ ∃𝑥∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝜑))} |
24 | | df-oprab 5855 |
. 2
⊢
{〈〈𝑥,
𝑦〉, 𝑧〉 ∣ 𝜑} = {𝑣 ∣ ∃𝑥∃𝑦∃𝑧(𝑣 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑)} |
25 | | df-opab 4049 |
. 2
⊢
{〈𝑤, 𝑧〉 ∣ ∃𝑥∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝜑)} = {𝑣 ∣ ∃𝑤∃𝑧(𝑣 = 〈𝑤, 𝑧〉 ∧ ∃𝑥∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝜑))} |
26 | 23, 24, 25 | 3eqtr4i 2201 |
1
⊢
{〈〈𝑥,
𝑦〉, 𝑧〉 ∣ 𝜑} = {〈𝑤, 𝑧〉 ∣ ∃𝑥∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝜑)} |