Step | Hyp | Ref
| Expression |
1 | | vex 2715 |
. . . 4
⊢ 𝑥 ∈ V |
2 | | vex 2715 |
. . . 4
⊢ 𝑦 ∈ V |
3 | 1, 2 | opex 4189 |
. . 3
⊢
〈𝑥, 𝑦〉 ∈ V |
4 | | vex 2715 |
. . 3
⊢ 𝑧 ∈ V |
5 | | opexg 4188 |
. . 3
⊢
((〈𝑥, 𝑦〉 ∈ V ∧ 𝑧 ∈ V) →
〈〈𝑥, 𝑦〉, 𝑧〉 ∈ V) |
6 | 3, 4, 5 | mp2an 423 |
. 2
⊢
〈〈𝑥, 𝑦〉, 𝑧〉 ∈ V |
7 | 3, 4 | eqvinop 4203 |
. . . . 5
⊢ (𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ↔ ∃𝑎∃𝑡(𝑤 = 〈𝑎, 𝑡〉 ∧ 〈𝑎, 𝑡〉 = 〈〈𝑥, 𝑦〉, 𝑧〉)) |
8 | 7 | biimpi 119 |
. . . 4
⊢ (𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 → ∃𝑎∃𝑡(𝑤 = 〈𝑎, 𝑡〉 ∧ 〈𝑎, 𝑡〉 = 〈〈𝑥, 𝑦〉, 𝑧〉)) |
9 | | eqeq1 2164 |
. . . . . . . 8
⊢ (𝑤 = 〈𝑎, 𝑡〉 → (𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ↔ 〈𝑎, 𝑡〉 = 〈〈𝑥, 𝑦〉, 𝑧〉)) |
10 | | vex 2715 |
. . . . . . . . 9
⊢ 𝑎 ∈ V |
11 | | vex 2715 |
. . . . . . . . 9
⊢ 𝑡 ∈ V |
12 | 10, 11 | opth1 4196 |
. . . . . . . 8
⊢
(〈𝑎, 𝑡〉 = 〈〈𝑥, 𝑦〉, 𝑧〉 → 𝑎 = 〈𝑥, 𝑦〉) |
13 | 9, 12 | syl6bi 162 |
. . . . . . 7
⊢ (𝑤 = 〈𝑎, 𝑡〉 → (𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 → 𝑎 = 〈𝑥, 𝑦〉)) |
14 | 1, 2 | eqvinop 4203 |
. . . . . . . . 9
⊢ (𝑎 = 〈𝑥, 𝑦〉 ↔ ∃𝑟∃𝑠(𝑎 = 〈𝑟, 𝑠〉 ∧ 〈𝑟, 𝑠〉 = 〈𝑥, 𝑦〉)) |
15 | | opeq1 3741 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 〈𝑟, 𝑠〉 → 〈𝑎, 𝑡〉 = 〈〈𝑟, 𝑠〉, 𝑡〉) |
16 | 15 | eqeq2d 2169 |
. . . . . . . . . . . 12
⊢ (𝑎 = 〈𝑟, 𝑠〉 → (𝑤 = 〈𝑎, 𝑡〉 ↔ 𝑤 = 〈〈𝑟, 𝑠〉, 𝑡〉)) |
17 | 1, 2, 4 | otth2 4201 |
. . . . . . . . . . . . . . . . . . 19
⊢
(〈〈𝑥,
𝑦〉, 𝑧〉 = 〈〈𝑟, 𝑠〉, 𝑡〉 ↔ (𝑥 = 𝑟 ∧ 𝑦 = 𝑠 ∧ 𝑧 = 𝑡)) |
18 | | df-3an 965 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 = 𝑟 ∧ 𝑦 = 𝑠 ∧ 𝑧 = 𝑡) ↔ ((𝑥 = 𝑟 ∧ 𝑦 = 𝑠) ∧ 𝑧 = 𝑡)) |
19 | 17, 18 | bitri 183 |
. . . . . . . . . . . . . . . . . 18
⊢
(〈〈𝑥,
𝑦〉, 𝑧〉 = 〈〈𝑟, 𝑠〉, 𝑡〉 ↔ ((𝑥 = 𝑟 ∧ 𝑦 = 𝑠) ∧ 𝑧 = 𝑡)) |
20 | 19 | anbi1i 454 |
. . . . . . . . . . . . . . . . 17
⊢
((〈〈𝑥,
𝑦〉, 𝑧〉 = 〈〈𝑟, 𝑠〉, 𝑡〉 ∧ 𝜑) ↔ (((𝑥 = 𝑟 ∧ 𝑦 = 𝑠) ∧ 𝑧 = 𝑡) ∧ 𝜑)) |
21 | | anass 399 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑥 = 𝑟 ∧ 𝑦 = 𝑠) ∧ 𝑧 = 𝑡) ∧ 𝜑) ↔ ((𝑥 = 𝑟 ∧ 𝑦 = 𝑠) ∧ (𝑧 = 𝑡 ∧ 𝜑))) |
22 | | anass 399 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 = 𝑟 ∧ 𝑦 = 𝑠) ∧ (𝑧 = 𝑡 ∧ 𝜑)) ↔ (𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑)))) |
23 | 20, 21, 22 | 3bitri 205 |
. . . . . . . . . . . . . . . 16
⊢
((〈〈𝑥,
𝑦〉, 𝑧〉 = 〈〈𝑟, 𝑠〉, 𝑡〉 ∧ 𝜑) ↔ (𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑)))) |
24 | 23 | 3exbii 1587 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑥∃𝑦∃𝑧(〈〈𝑥, 𝑦〉, 𝑧〉 = 〈〈𝑟, 𝑠〉, 𝑡〉 ∧ 𝜑) ↔ ∃𝑥∃𝑦∃𝑧(𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑)))) |
25 | | oprabidlem 5852 |
. . . . . . . . . . . . . . . . . 18
⊢
(∃𝑥∃𝑧(𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) → ∃𝑥(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑)))) |
26 | 25 | eximi 1580 |
. . . . . . . . . . . . . . . . 17
⊢
(∃𝑦∃𝑥∃𝑧(𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) → ∃𝑦∃𝑥(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑)))) |
27 | | excom 1644 |
. . . . . . . . . . . . . . . . 17
⊢
(∃𝑥∃𝑦∃𝑧(𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) ↔ ∃𝑦∃𝑥∃𝑧(𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑)))) |
28 | | excom 1644 |
. . . . . . . . . . . . . . . . 17
⊢
(∃𝑥∃𝑦(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) ↔ ∃𝑦∃𝑥(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑)))) |
29 | 26, 27, 28 | 3imtr4i 200 |
. . . . . . . . . . . . . . . 16
⊢
(∃𝑥∃𝑦∃𝑧(𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) → ∃𝑥∃𝑦(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑)))) |
30 | | oprabidlem 5852 |
. . . . . . . . . . . . . . . 16
⊢
(∃𝑥∃𝑦(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) → ∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑)))) |
31 | | oprabidlem 5852 |
. . . . . . . . . . . . . . . . . 18
⊢
(∃𝑦∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑)) → ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑))) |
32 | 31 | anim2i 340 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 = 𝑟 ∧ ∃𝑦∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) → (𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑)))) |
33 | 32 | eximi 1580 |
. . . . . . . . . . . . . . . 16
⊢
(∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) → ∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑)))) |
34 | 29, 30, 33 | 3syl 17 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑥∃𝑦∃𝑧(𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) → ∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑)))) |
35 | 24, 34 | sylbi 120 |
. . . . . . . . . . . . . 14
⊢
(∃𝑥∃𝑦∃𝑧(〈〈𝑥, 𝑦〉, 𝑧〉 = 〈〈𝑟, 𝑠〉, 𝑡〉 ∧ 𝜑) → ∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑)))) |
36 | | euequ1 2101 |
. . . . . . . . . . . . . . . . . . 19
⊢
∃!𝑥 𝑥 = 𝑟 |
37 | | eupick 2085 |
. . . . . . . . . . . . . . . . . . 19
⊢
((∃!𝑥 𝑥 = 𝑟 ∧ ∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑)))) → (𝑥 = 𝑟 → ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑)))) |
38 | 36, 37 | mpan 421 |
. . . . . . . . . . . . . . . . . 18
⊢
(∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑))) → (𝑥 = 𝑟 → ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑)))) |
39 | | euequ1 2101 |
. . . . . . . . . . . . . . . . . . . 20
⊢
∃!𝑦 𝑦 = 𝑠 |
40 | | eupick 2085 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((∃!𝑦 𝑦 = 𝑠 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑))) → (𝑦 = 𝑠 → ∃𝑧(𝑧 = 𝑡 ∧ 𝜑))) |
41 | 39, 40 | mpan 421 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑)) → (𝑦 = 𝑠 → ∃𝑧(𝑧 = 𝑡 ∧ 𝜑))) |
42 | | euequ1 2101 |
. . . . . . . . . . . . . . . . . . . 20
⊢
∃!𝑧 𝑧 = 𝑡 |
43 | | eupick 2085 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((∃!𝑧 𝑧 = 𝑡 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑)) → (𝑧 = 𝑡 → 𝜑)) |
44 | 42, 43 | mpan 421 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∃𝑧(𝑧 = 𝑡 ∧ 𝜑) → (𝑧 = 𝑡 → 𝜑)) |
45 | 41, 44 | syl6 33 |
. . . . . . . . . . . . . . . . . 18
⊢
(∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑)) → (𝑦 = 𝑠 → (𝑧 = 𝑡 → 𝜑))) |
46 | 38, 45 | syl6 33 |
. . . . . . . . . . . . . . . . 17
⊢
(∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑))) → (𝑥 = 𝑟 → (𝑦 = 𝑠 → (𝑧 = 𝑡 → 𝜑)))) |
47 | 46 | 3impd 1203 |
. . . . . . . . . . . . . . . 16
⊢
(∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑))) → ((𝑥 = 𝑟 ∧ 𝑦 = 𝑠 ∧ 𝑧 = 𝑡) → 𝜑)) |
48 | 17, 47 | syl5bi 151 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑))) → (〈〈𝑥, 𝑦〉, 𝑧〉 = 〈〈𝑟, 𝑠〉, 𝑡〉 → 𝜑)) |
49 | 48 | com12 30 |
. . . . . . . . . . . . . 14
⊢
(〈〈𝑥,
𝑦〉, 𝑧〉 = 〈〈𝑟, 𝑠〉, 𝑡〉 → (∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑))) → 𝜑)) |
50 | 35, 49 | syl5 32 |
. . . . . . . . . . . . 13
⊢
(〈〈𝑥,
𝑦〉, 𝑧〉 = 〈〈𝑟, 𝑠〉, 𝑡〉 → (∃𝑥∃𝑦∃𝑧(〈〈𝑥, 𝑦〉, 𝑧〉 = 〈〈𝑟, 𝑠〉, 𝑡〉 ∧ 𝜑) → 𝜑)) |
51 | | eqeq1 2164 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = 〈〈𝑟, 𝑠〉, 𝑡〉 → (𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ↔ 〈〈𝑟, 𝑠〉, 𝑡〉 = 〈〈𝑥, 𝑦〉, 𝑧〉)) |
52 | | eqcom 2159 |
. . . . . . . . . . . . . . 15
⊢
(〈〈𝑟,
𝑠〉, 𝑡〉 = 〈〈𝑥, 𝑦〉, 𝑧〉 ↔ 〈〈𝑥, 𝑦〉, 𝑧〉 = 〈〈𝑟, 𝑠〉, 𝑡〉) |
53 | 51, 52 | bitrdi 195 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = 〈〈𝑟, 𝑠〉, 𝑡〉 → (𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ↔ 〈〈𝑥, 𝑦〉, 𝑧〉 = 〈〈𝑟, 𝑠〉, 𝑡〉)) |
54 | 53 | anbi1d 461 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = 〈〈𝑟, 𝑠〉, 𝑡〉 → ((𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) ↔ (〈〈𝑥, 𝑦〉, 𝑧〉 = 〈〈𝑟, 𝑠〉, 𝑡〉 ∧ 𝜑))) |
55 | 54 | 3exbidv 1849 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = 〈〈𝑟, 𝑠〉, 𝑡〉 → (∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) ↔ ∃𝑥∃𝑦∃𝑧(〈〈𝑥, 𝑦〉, 𝑧〉 = 〈〈𝑟, 𝑠〉, 𝑡〉 ∧ 𝜑))) |
56 | 55 | imbi1d 230 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = 〈〈𝑟, 𝑠〉, 𝑡〉 → ((∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) → 𝜑) ↔ (∃𝑥∃𝑦∃𝑧(〈〈𝑥, 𝑦〉, 𝑧〉 = 〈〈𝑟, 𝑠〉, 𝑡〉 ∧ 𝜑) → 𝜑))) |
57 | 53, 56 | imbi12d 233 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 〈〈𝑟, 𝑠〉, 𝑡〉 → ((𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 → (∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) → 𝜑)) ↔ (〈〈𝑥, 𝑦〉, 𝑧〉 = 〈〈𝑟, 𝑠〉, 𝑡〉 → (∃𝑥∃𝑦∃𝑧(〈〈𝑥, 𝑦〉, 𝑧〉 = 〈〈𝑟, 𝑠〉, 𝑡〉 ∧ 𝜑) → 𝜑)))) |
58 | 50, 57 | mpbiri 167 |
. . . . . . . . . . . 12
⊢ (𝑤 = 〈〈𝑟, 𝑠〉, 𝑡〉 → (𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 → (∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) → 𝜑))) |
59 | 16, 58 | syl6bi 162 |
. . . . . . . . . . 11
⊢ (𝑎 = 〈𝑟, 𝑠〉 → (𝑤 = 〈𝑎, 𝑡〉 → (𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 → (∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) → 𝜑)))) |
60 | 59 | adantr 274 |
. . . . . . . . . 10
⊢ ((𝑎 = 〈𝑟, 𝑠〉 ∧ 〈𝑟, 𝑠〉 = 〈𝑥, 𝑦〉) → (𝑤 = 〈𝑎, 𝑡〉 → (𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 → (∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) → 𝜑)))) |
61 | 60 | exlimivv 1876 |
. . . . . . . . 9
⊢
(∃𝑟∃𝑠(𝑎 = 〈𝑟, 𝑠〉 ∧ 〈𝑟, 𝑠〉 = 〈𝑥, 𝑦〉) → (𝑤 = 〈𝑎, 𝑡〉 → (𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 → (∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) → 𝜑)))) |
62 | 14, 61 | sylbi 120 |
. . . . . . . 8
⊢ (𝑎 = 〈𝑥, 𝑦〉 → (𝑤 = 〈𝑎, 𝑡〉 → (𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 → (∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) → 𝜑)))) |
63 | 62 | com3l 81 |
. . . . . . 7
⊢ (𝑤 = 〈𝑎, 𝑡〉 → (𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 → (𝑎 = 〈𝑥, 𝑦〉 → (∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) → 𝜑)))) |
64 | 13, 63 | mpdd 41 |
. . . . . 6
⊢ (𝑤 = 〈𝑎, 𝑡〉 → (𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 → (∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) → 𝜑))) |
65 | 64 | adantr 274 |
. . . . 5
⊢ ((𝑤 = 〈𝑎, 𝑡〉 ∧ 〈𝑎, 𝑡〉 = 〈〈𝑥, 𝑦〉, 𝑧〉) → (𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 → (∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) → 𝜑))) |
66 | 65 | exlimivv 1876 |
. . . 4
⊢
(∃𝑎∃𝑡(𝑤 = 〈𝑎, 𝑡〉 ∧ 〈𝑎, 𝑡〉 = 〈〈𝑥, 𝑦〉, 𝑧〉) → (𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 → (∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) → 𝜑))) |
67 | 8, 66 | mpcom 36 |
. . 3
⊢ (𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 → (∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) → 𝜑)) |
68 | | 19.8a 1570 |
. . . . 5
⊢ ((𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) → ∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑)) |
69 | | 19.8a 1570 |
. . . . 5
⊢
(∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) → ∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑)) |
70 | | 19.8a 1570 |
. . . . 5
⊢
(∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) → ∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑)) |
71 | 68, 69, 70 | 3syl 17 |
. . . 4
⊢ ((𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) → ∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑)) |
72 | 71 | ex 114 |
. . 3
⊢ (𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 → (𝜑 → ∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑))) |
73 | 67, 72 | impbid 128 |
. 2
⊢ (𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 → (∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) ↔ 𝜑)) |
74 | | df-oprab 5828 |
. 2
⊢
{〈〈𝑥,
𝑦〉, 𝑧〉 ∣ 𝜑} = {𝑤 ∣ ∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑)} |
75 | 6, 73, 74 | elab2 2860 |
1
⊢
(〈〈𝑥,
𝑦〉, 𝑧〉 ∈ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} ↔ 𝜑) |