| Step | Hyp | Ref
| Expression |
| 1 | | elxp 5708 |
. 2
⊢ (𝐴 ∈ ((V × V) ×
V) ↔ ∃𝑤∃𝑧(𝐴 = 〈𝑤, 𝑧〉 ∧ (𝑤 ∈ (V × V) ∧ 𝑧 ∈ V))) |
| 2 | | ancom 460 |
. . . . . 6
⊢ ((𝑤 = 〈𝑥, 𝑦〉 ∧ 𝐴 = 〈𝑤, 𝑧〉) ↔ (𝐴 = 〈𝑤, 𝑧〉 ∧ 𝑤 = 〈𝑥, 𝑦〉)) |
| 3 | 2 | 2exbii 1849 |
. . . . 5
⊢
(∃𝑥∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝐴 = 〈𝑤, 𝑧〉) ↔ ∃𝑥∃𝑦(𝐴 = 〈𝑤, 𝑧〉 ∧ 𝑤 = 〈𝑥, 𝑦〉)) |
| 4 | | 19.42vv 1957 |
. . . . . 6
⊢
(∃𝑥∃𝑦(𝐴 = 〈𝑤, 𝑧〉 ∧ 𝑤 = 〈𝑥, 𝑦〉) ↔ (𝐴 = 〈𝑤, 𝑧〉 ∧ ∃𝑥∃𝑦 𝑤 = 〈𝑥, 𝑦〉)) |
| 5 | | elvv 5760 |
. . . . . . 7
⊢ (𝑤 ∈ (V × V) ↔
∃𝑥∃𝑦 𝑤 = 〈𝑥, 𝑦〉) |
| 6 | 5 | anbi2i 623 |
. . . . . 6
⊢ ((𝐴 = 〈𝑤, 𝑧〉 ∧ 𝑤 ∈ (V × V)) ↔ (𝐴 = 〈𝑤, 𝑧〉 ∧ ∃𝑥∃𝑦 𝑤 = 〈𝑥, 𝑦〉)) |
| 7 | | vex 3484 |
. . . . . . 7
⊢ 𝑧 ∈ V |
| 8 | 7 | biantru 529 |
. . . . . 6
⊢ ((𝐴 = 〈𝑤, 𝑧〉 ∧ 𝑤 ∈ (V × V)) ↔ ((𝐴 = 〈𝑤, 𝑧〉 ∧ 𝑤 ∈ (V × V)) ∧ 𝑧 ∈ V)) |
| 9 | 4, 6, 8 | 3bitr2i 299 |
. . . . 5
⊢
(∃𝑥∃𝑦(𝐴 = 〈𝑤, 𝑧〉 ∧ 𝑤 = 〈𝑥, 𝑦〉) ↔ ((𝐴 = 〈𝑤, 𝑧〉 ∧ 𝑤 ∈ (V × V)) ∧ 𝑧 ∈ V)) |
| 10 | | anass 468 |
. . . . 5
⊢ (((𝐴 = 〈𝑤, 𝑧〉 ∧ 𝑤 ∈ (V × V)) ∧ 𝑧 ∈ V) ↔ (𝐴 = 〈𝑤, 𝑧〉 ∧ (𝑤 ∈ (V × V) ∧ 𝑧 ∈ V))) |
| 11 | 3, 9, 10 | 3bitrri 298 |
. . . 4
⊢ ((𝐴 = 〈𝑤, 𝑧〉 ∧ (𝑤 ∈ (V × V) ∧ 𝑧 ∈ V)) ↔ ∃𝑥∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝐴 = 〈𝑤, 𝑧〉)) |
| 12 | 11 | 2exbii 1849 |
. . 3
⊢
(∃𝑤∃𝑧(𝐴 = 〈𝑤, 𝑧〉 ∧ (𝑤 ∈ (V × V) ∧ 𝑧 ∈ V)) ↔ ∃𝑤∃𝑧∃𝑥∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝐴 = 〈𝑤, 𝑧〉)) |
| 13 | | exrot4 2166 |
. . 3
⊢
(∃𝑥∃𝑦∃𝑤∃𝑧(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝐴 = 〈𝑤, 𝑧〉) ↔ ∃𝑤∃𝑧∃𝑥∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝐴 = 〈𝑤, 𝑧〉)) |
| 14 | | excom 2162 |
. . . . 5
⊢
(∃𝑤∃𝑧(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝐴 = 〈𝑤, 𝑧〉) ↔ ∃𝑧∃𝑤(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝐴 = 〈𝑤, 𝑧〉)) |
| 15 | | opex 5469 |
. . . . . . 7
⊢
〈𝑥, 𝑦〉 ∈ V |
| 16 | | opeq1 4873 |
. . . . . . . 8
⊢ (𝑤 = 〈𝑥, 𝑦〉 → 〈𝑤, 𝑧〉 = 〈〈𝑥, 𝑦〉, 𝑧〉) |
| 17 | 16 | eqeq2d 2748 |
. . . . . . 7
⊢ (𝑤 = 〈𝑥, 𝑦〉 → (𝐴 = 〈𝑤, 𝑧〉 ↔ 𝐴 = 〈〈𝑥, 𝑦〉, 𝑧〉)) |
| 18 | 15, 17 | ceqsexv 3532 |
. . . . . 6
⊢
(∃𝑤(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝐴 = 〈𝑤, 𝑧〉) ↔ 𝐴 = 〈〈𝑥, 𝑦〉, 𝑧〉) |
| 19 | 18 | exbii 1848 |
. . . . 5
⊢
(∃𝑧∃𝑤(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝐴 = 〈𝑤, 𝑧〉) ↔ ∃𝑧 𝐴 = 〈〈𝑥, 𝑦〉, 𝑧〉) |
| 20 | 14, 19 | bitri 275 |
. . . 4
⊢
(∃𝑤∃𝑧(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝐴 = 〈𝑤, 𝑧〉) ↔ ∃𝑧 𝐴 = 〈〈𝑥, 𝑦〉, 𝑧〉) |
| 21 | 20 | 2exbii 1849 |
. . 3
⊢
(∃𝑥∃𝑦∃𝑤∃𝑧(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝐴 = 〈𝑤, 𝑧〉) ↔ ∃𝑥∃𝑦∃𝑧 𝐴 = 〈〈𝑥, 𝑦〉, 𝑧〉) |
| 22 | 12, 13, 21 | 3bitr2i 299 |
. 2
⊢
(∃𝑤∃𝑧(𝐴 = 〈𝑤, 𝑧〉 ∧ (𝑤 ∈ (V × V) ∧ 𝑧 ∈ V)) ↔ ∃𝑥∃𝑦∃𝑧 𝐴 = 〈〈𝑥, 𝑦〉, 𝑧〉) |
| 23 | 1, 22 | bitri 275 |
1
⊢ (𝐴 ∈ ((V × V) ×
V) ↔ ∃𝑥∃𝑦∃𝑧 𝐴 = 〈〈𝑥, 𝑦〉, 𝑧〉) |