Step | Hyp | Ref
| Expression |
1 | | opex 5323 |
. 2
⊢
〈〈𝑥, 𝑦〉, 𝑧〉 ∈ V |
2 | | opex 5323 |
. . . . . 6
⊢
〈𝑥, 𝑦〉 ∈ V |
3 | | vex 3402 |
. . . . . 6
⊢ 𝑧 ∈ V |
4 | 2, 3 | eqvinop 5345 |
. . . . 5
⊢ (𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ↔ ∃𝑎∃𝑡(𝑤 = 〈𝑎, 𝑡〉 ∧ 〈𝑎, 𝑡〉 = 〈〈𝑥, 𝑦〉, 𝑧〉)) |
5 | 4 | biimpi 219 |
. . . 4
⊢ (𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 → ∃𝑎∃𝑡(𝑤 = 〈𝑎, 𝑡〉 ∧ 〈𝑎, 𝑡〉 = 〈〈𝑥, 𝑦〉, 𝑧〉)) |
6 | | eqeq1 2742 |
. . . . . . . 8
⊢ (𝑤 = 〈𝑎, 𝑡〉 → (𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ↔ 〈𝑎, 𝑡〉 = 〈〈𝑥, 𝑦〉, 𝑧〉)) |
7 | | vex 3402 |
. . . . . . . . 9
⊢ 𝑎 ∈ V |
8 | | vex 3402 |
. . . . . . . . 9
⊢ 𝑡 ∈ V |
9 | 7, 8 | opth1 5334 |
. . . . . . . 8
⊢
(〈𝑎, 𝑡〉 = 〈〈𝑥, 𝑦〉, 𝑧〉 → 𝑎 = 〈𝑥, 𝑦〉) |
10 | 6, 9 | syl6bi 256 |
. . . . . . 7
⊢ (𝑤 = 〈𝑎, 𝑡〉 → (𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 → 𝑎 = 〈𝑥, 𝑦〉)) |
11 | | vex 3402 |
. . . . . . . . . 10
⊢ 𝑥 ∈ V |
12 | | vex 3402 |
. . . . . . . . . 10
⊢ 𝑦 ∈ V |
13 | 11, 12 | eqvinop 5345 |
. . . . . . . . 9
⊢ (𝑎 = 〈𝑥, 𝑦〉 ↔ ∃𝑟∃𝑠(𝑎 = 〈𝑟, 𝑠〉 ∧ 〈𝑟, 𝑠〉 = 〈𝑥, 𝑦〉)) |
14 | | opeq1 4760 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 〈𝑟, 𝑠〉 → 〈𝑎, 𝑡〉 = 〈〈𝑟, 𝑠〉, 𝑡〉) |
15 | 14 | eqeq2d 2749 |
. . . . . . . . . . . 12
⊢ (𝑎 = 〈𝑟, 𝑠〉 → (𝑤 = 〈𝑎, 𝑡〉 ↔ 𝑤 = 〈〈𝑟, 𝑠〉, 𝑡〉)) |
16 | 11, 12, 3 | otth2 5342 |
. . . . . . . . . . . . . . 15
⊢
(〈〈𝑥,
𝑦〉, 𝑧〉 = 〈〈𝑟, 𝑠〉, 𝑡〉 ↔ (𝑥 = 𝑟 ∧ 𝑦 = 𝑠 ∧ 𝑧 = 𝑡)) |
17 | | euequ 2598 |
. . . . . . . . . . . . . . . . . 18
⊢
∃!𝑥 𝑥 = 𝑟 |
18 | | eupick 2636 |
. . . . . . . . . . . . . . . . . 18
⊢
((∃!𝑥 𝑥 = 𝑟 ∧ ∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑)))) → (𝑥 = 𝑟 → ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑)))) |
19 | 17, 18 | mpan 690 |
. . . . . . . . . . . . . . . . 17
⊢
(∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑))) → (𝑥 = 𝑟 → ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑)))) |
20 | | euequ 2598 |
. . . . . . . . . . . . . . . . . . 19
⊢
∃!𝑦 𝑦 = 𝑠 |
21 | | eupick 2636 |
. . . . . . . . . . . . . . . . . . 19
⊢
((∃!𝑦 𝑦 = 𝑠 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑))) → (𝑦 = 𝑠 → ∃𝑧(𝑧 = 𝑡 ∧ 𝜑))) |
22 | 20, 21 | mpan 690 |
. . . . . . . . . . . . . . . . . 18
⊢
(∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑)) → (𝑦 = 𝑠 → ∃𝑧(𝑧 = 𝑡 ∧ 𝜑))) |
23 | | euequ 2598 |
. . . . . . . . . . . . . . . . . . 19
⊢
∃!𝑧 𝑧 = 𝑡 |
24 | | eupick 2636 |
. . . . . . . . . . . . . . . . . . 19
⊢
((∃!𝑧 𝑧 = 𝑡 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑)) → (𝑧 = 𝑡 → 𝜑)) |
25 | 23, 24 | mpan 690 |
. . . . . . . . . . . . . . . . . 18
⊢
(∃𝑧(𝑧 = 𝑡 ∧ 𝜑) → (𝑧 = 𝑡 → 𝜑)) |
26 | 22, 25 | syl6 35 |
. . . . . . . . . . . . . . . . 17
⊢
(∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑)) → (𝑦 = 𝑠 → (𝑧 = 𝑡 → 𝜑))) |
27 | 19, 26 | syl6 35 |
. . . . . . . . . . . . . . . 16
⊢
(∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑))) → (𝑥 = 𝑟 → (𝑦 = 𝑠 → (𝑧 = 𝑡 → 𝜑)))) |
28 | 27 | 3impd 1349 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑))) → ((𝑥 = 𝑟 ∧ 𝑦 = 𝑠 ∧ 𝑧 = 𝑡) → 𝜑)) |
29 | 16, 28 | syl5bi 245 |
. . . . . . . . . . . . . 14
⊢
(∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑))) → (〈〈𝑥, 𝑦〉, 𝑧〉 = 〈〈𝑟, 𝑠〉, 𝑡〉 → 𝜑)) |
30 | | df-3an 1090 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 = 𝑟 ∧ 𝑦 = 𝑠 ∧ 𝑧 = 𝑡) ↔ ((𝑥 = 𝑟 ∧ 𝑦 = 𝑠) ∧ 𝑧 = 𝑡)) |
31 | 16, 30 | bitri 278 |
. . . . . . . . . . . . . . . . . 18
⊢
(〈〈𝑥,
𝑦〉, 𝑧〉 = 〈〈𝑟, 𝑠〉, 𝑡〉 ↔ ((𝑥 = 𝑟 ∧ 𝑦 = 𝑠) ∧ 𝑧 = 𝑡)) |
32 | 31 | anbi1i 627 |
. . . . . . . . . . . . . . . . 17
⊢
((〈〈𝑥,
𝑦〉, 𝑧〉 = 〈〈𝑟, 𝑠〉, 𝑡〉 ∧ 𝜑) ↔ (((𝑥 = 𝑟 ∧ 𝑦 = 𝑠) ∧ 𝑧 = 𝑡) ∧ 𝜑)) |
33 | | anass 472 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑥 = 𝑟 ∧ 𝑦 = 𝑠) ∧ 𝑧 = 𝑡) ∧ 𝜑) ↔ ((𝑥 = 𝑟 ∧ 𝑦 = 𝑠) ∧ (𝑧 = 𝑡 ∧ 𝜑))) |
34 | | anass 472 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 = 𝑟 ∧ 𝑦 = 𝑠) ∧ (𝑧 = 𝑡 ∧ 𝜑)) ↔ (𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑)))) |
35 | 32, 33, 34 | 3bitri 300 |
. . . . . . . . . . . . . . . 16
⊢
((〈〈𝑥,
𝑦〉, 𝑧〉 = 〈〈𝑟, 𝑠〉, 𝑡〉 ∧ 𝜑) ↔ (𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑)))) |
36 | 35 | 3exbii 1856 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑥∃𝑦∃𝑧(〈〈𝑥, 𝑦〉, 𝑧〉 = 〈〈𝑟, 𝑠〉, 𝑡〉 ∧ 𝜑) ↔ ∃𝑥∃𝑦∃𝑧(𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑)))) |
37 | | nfcvf2 2929 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (¬
∀𝑥 𝑥 = 𝑧 → Ⅎ𝑧𝑥) |
38 | | nfcvd 2900 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (¬
∀𝑥 𝑥 = 𝑧 → Ⅎ𝑧𝑟) |
39 | 37, 38 | nfeqd 2909 |
. . . . . . . . . . . . . . . . . . 19
⊢ (¬
∀𝑥 𝑥 = 𝑧 → Ⅎ𝑧 𝑥 = 𝑟) |
40 | 39 | exdistrf 2446 |
. . . . . . . . . . . . . . . . . 18
⊢
(∃𝑥∃𝑧(𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) → ∃𝑥(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑)))) |
41 | 40 | eximi 1841 |
. . . . . . . . . . . . . . . . 17
⊢
(∃𝑦∃𝑥∃𝑧(𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) → ∃𝑦∃𝑥(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑)))) |
42 | | excom 2169 |
. . . . . . . . . . . . . . . . 17
⊢
(∃𝑥∃𝑦∃𝑧(𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) ↔ ∃𝑦∃𝑥∃𝑧(𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑)))) |
43 | | excom 2169 |
. . . . . . . . . . . . . . . . 17
⊢
(∃𝑥∃𝑦(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) ↔ ∃𝑦∃𝑥(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑)))) |
44 | 41, 42, 43 | 3imtr4i 295 |
. . . . . . . . . . . . . . . 16
⊢
(∃𝑥∃𝑦∃𝑧(𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) → ∃𝑥∃𝑦(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑)))) |
45 | | nfcvf2 2929 |
. . . . . . . . . . . . . . . . . 18
⊢ (¬
∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦𝑥) |
46 | | nfcvd 2900 |
. . . . . . . . . . . . . . . . . 18
⊢ (¬
∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦𝑟) |
47 | 45, 46 | nfeqd 2909 |
. . . . . . . . . . . . . . . . 17
⊢ (¬
∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦 𝑥 = 𝑟) |
48 | 47 | exdistrf 2446 |
. . . . . . . . . . . . . . . 16
⊢
(∃𝑥∃𝑦(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) → ∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑)))) |
49 | | nfcvf2 2929 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (¬
∀𝑦 𝑦 = 𝑧 → Ⅎ𝑧𝑦) |
50 | | nfcvd 2900 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (¬
∀𝑦 𝑦 = 𝑧 → Ⅎ𝑧𝑠) |
51 | 49, 50 | nfeqd 2909 |
. . . . . . . . . . . . . . . . . . 19
⊢ (¬
∀𝑦 𝑦 = 𝑧 → Ⅎ𝑧 𝑦 = 𝑠) |
52 | 51 | exdistrf 2446 |
. . . . . . . . . . . . . . . . . 18
⊢
(∃𝑦∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑)) → ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑))) |
53 | 52 | anim2i 620 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 = 𝑟 ∧ ∃𝑦∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) → (𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑)))) |
54 | 53 | eximi 1841 |
. . . . . . . . . . . . . . . 16
⊢
(∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) → ∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑)))) |
55 | 44, 48, 54 | 3syl 18 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑥∃𝑦∃𝑧(𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) → ∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑)))) |
56 | 36, 55 | sylbi 220 |
. . . . . . . . . . . . . 14
⊢
(∃𝑥∃𝑦∃𝑧(〈〈𝑥, 𝑦〉, 𝑧〉 = 〈〈𝑟, 𝑠〉, 𝑡〉 ∧ 𝜑) → ∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑)))) |
57 | 29, 56 | syl11 33 |
. . . . . . . . . . . . 13
⊢
(〈〈𝑥,
𝑦〉, 𝑧〉 = 〈〈𝑟, 𝑠〉, 𝑡〉 → (∃𝑥∃𝑦∃𝑧(〈〈𝑥, 𝑦〉, 𝑧〉 = 〈〈𝑟, 𝑠〉, 𝑡〉 ∧ 𝜑) → 𝜑)) |
58 | | eqeq1 2742 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = 〈〈𝑟, 𝑠〉, 𝑡〉 → (𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ↔ 〈〈𝑟, 𝑠〉, 𝑡〉 = 〈〈𝑥, 𝑦〉, 𝑧〉)) |
59 | | eqcom 2745 |
. . . . . . . . . . . . . . 15
⊢
(〈〈𝑟,
𝑠〉, 𝑡〉 = 〈〈𝑥, 𝑦〉, 𝑧〉 ↔ 〈〈𝑥, 𝑦〉, 𝑧〉 = 〈〈𝑟, 𝑠〉, 𝑡〉) |
60 | 58, 59 | bitrdi 290 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = 〈〈𝑟, 𝑠〉, 𝑡〉 → (𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ↔ 〈〈𝑥, 𝑦〉, 𝑧〉 = 〈〈𝑟, 𝑠〉, 𝑡〉)) |
61 | 60 | anbi1d 633 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = 〈〈𝑟, 𝑠〉, 𝑡〉 → ((𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) ↔ (〈〈𝑥, 𝑦〉, 𝑧〉 = 〈〈𝑟, 𝑠〉, 𝑡〉 ∧ 𝜑))) |
62 | 61 | 3exbidv 1931 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = 〈〈𝑟, 𝑠〉, 𝑡〉 → (∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) ↔ ∃𝑥∃𝑦∃𝑧(〈〈𝑥, 𝑦〉, 𝑧〉 = 〈〈𝑟, 𝑠〉, 𝑡〉 ∧ 𝜑))) |
63 | 62 | imbi1d 345 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = 〈〈𝑟, 𝑠〉, 𝑡〉 → ((∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) → 𝜑) ↔ (∃𝑥∃𝑦∃𝑧(〈〈𝑥, 𝑦〉, 𝑧〉 = 〈〈𝑟, 𝑠〉, 𝑡〉 ∧ 𝜑) → 𝜑))) |
64 | 60, 63 | imbi12d 348 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 〈〈𝑟, 𝑠〉, 𝑡〉 → ((𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 → (∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) → 𝜑)) ↔ (〈〈𝑥, 𝑦〉, 𝑧〉 = 〈〈𝑟, 𝑠〉, 𝑡〉 → (∃𝑥∃𝑦∃𝑧(〈〈𝑥, 𝑦〉, 𝑧〉 = 〈〈𝑟, 𝑠〉, 𝑡〉 ∧ 𝜑) → 𝜑)))) |
65 | 57, 64 | mpbiri 261 |
. . . . . . . . . . . 12
⊢ (𝑤 = 〈〈𝑟, 𝑠〉, 𝑡〉 → (𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 → (∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) → 𝜑))) |
66 | 15, 65 | syl6bi 256 |
. . . . . . . . . . 11
⊢ (𝑎 = 〈𝑟, 𝑠〉 → (𝑤 = 〈𝑎, 𝑡〉 → (𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 → (∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) → 𝜑)))) |
67 | 66 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝑎 = 〈𝑟, 𝑠〉 ∧ 〈𝑟, 𝑠〉 = 〈𝑥, 𝑦〉) → (𝑤 = 〈𝑎, 𝑡〉 → (𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 → (∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) → 𝜑)))) |
68 | 67 | exlimivv 1938 |
. . . . . . . . 9
⊢
(∃𝑟∃𝑠(𝑎 = 〈𝑟, 𝑠〉 ∧ 〈𝑟, 𝑠〉 = 〈𝑥, 𝑦〉) → (𝑤 = 〈𝑎, 𝑡〉 → (𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 → (∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) → 𝜑)))) |
69 | 13, 68 | sylbi 220 |
. . . . . . . 8
⊢ (𝑎 = 〈𝑥, 𝑦〉 → (𝑤 = 〈𝑎, 𝑡〉 → (𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 → (∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) → 𝜑)))) |
70 | 69 | com3l 89 |
. . . . . . 7
⊢ (𝑤 = 〈𝑎, 𝑡〉 → (𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 → (𝑎 = 〈𝑥, 𝑦〉 → (∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) → 𝜑)))) |
71 | 10, 70 | mpdd 43 |
. . . . . 6
⊢ (𝑤 = 〈𝑎, 𝑡〉 → (𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 → (∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) → 𝜑))) |
72 | 71 | adantr 484 |
. . . . 5
⊢ ((𝑤 = 〈𝑎, 𝑡〉 ∧ 〈𝑎, 𝑡〉 = 〈〈𝑥, 𝑦〉, 𝑧〉) → (𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 → (∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) → 𝜑))) |
73 | 72 | exlimivv 1938 |
. . . 4
⊢
(∃𝑎∃𝑡(𝑤 = 〈𝑎, 𝑡〉 ∧ 〈𝑎, 𝑡〉 = 〈〈𝑥, 𝑦〉, 𝑧〉) → (𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 → (∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) → 𝜑))) |
74 | 5, 73 | mpcom 38 |
. . 3
⊢ (𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 → (∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) → 𝜑)) |
75 | | 19.8a 2181 |
. . . . 5
⊢ ((𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) → ∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑)) |
76 | | 19.8a 2181 |
. . . . 5
⊢
(∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) → ∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑)) |
77 | | 19.8a 2181 |
. . . . 5
⊢
(∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) → ∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑)) |
78 | 75, 76, 77 | 3syl 18 |
. . . 4
⊢ ((𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) → ∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑)) |
79 | 78 | ex 416 |
. . 3
⊢ (𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 → (𝜑 → ∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑))) |
80 | 74, 79 | impbid 215 |
. 2
⊢ (𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 → (∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) ↔ 𝜑)) |
81 | | df-oprab 7175 |
. 2
⊢
{〈〈𝑥,
𝑦〉, 𝑧〉 ∣ 𝜑} = {𝑤 ∣ ∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑)} |
82 | 1, 80, 81 | elab2 3577 |
1
⊢
(〈〈𝑥,
𝑦〉, 𝑧〉 ∈ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} ↔ 𝜑) |