Step | Hyp | Ref
| Expression |
1 | | opex 4859 |
. 2
⊢
〈〈𝑥, 𝑦〉, 𝑧〉 ∈ V |
2 | | opex 4859 |
. . . . . 6
⊢
〈𝑥, 𝑦〉 ∈ V |
3 | | vex 3176 |
. . . . . 6
⊢ 𝑧 ∈ V |
4 | 2, 3 | eqvinop 4881 |
. . . . 5
⊢ (𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ↔ ∃𝑎∃𝑡(𝑤 = 〈𝑎, 𝑡〉 ∧ 〈𝑎, 𝑡〉 = 〈〈𝑥, 𝑦〉, 𝑧〉)) |
5 | 4 | biimpi 205 |
. . . 4
⊢ (𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 → ∃𝑎∃𝑡(𝑤 = 〈𝑎, 𝑡〉 ∧ 〈𝑎, 𝑡〉 = 〈〈𝑥, 𝑦〉, 𝑧〉)) |
6 | | eqeq1 2614 |
. . . . . . . 8
⊢ (𝑤 = 〈𝑎, 𝑡〉 → (𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ↔ 〈𝑎, 𝑡〉 = 〈〈𝑥, 𝑦〉, 𝑧〉)) |
7 | | vex 3176 |
. . . . . . . . 9
⊢ 𝑎 ∈ V |
8 | | vex 3176 |
. . . . . . . . 9
⊢ 𝑡 ∈ V |
9 | 7, 8 | opth1 4870 |
. . . . . . . 8
⊢
(〈𝑎, 𝑡〉 = 〈〈𝑥, 𝑦〉, 𝑧〉 → 𝑎 = 〈𝑥, 𝑦〉) |
10 | 6, 9 | syl6bi 242 |
. . . . . . 7
⊢ (𝑤 = 〈𝑎, 𝑡〉 → (𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 → 𝑎 = 〈𝑥, 𝑦〉)) |
11 | | vex 3176 |
. . . . . . . . . 10
⊢ 𝑥 ∈ V |
12 | | vex 3176 |
. . . . . . . . . 10
⊢ 𝑦 ∈ V |
13 | 11, 12 | eqvinop 4881 |
. . . . . . . . 9
⊢ (𝑎 = 〈𝑥, 𝑦〉 ↔ ∃𝑟∃𝑠(𝑎 = 〈𝑟, 𝑠〉 ∧ 〈𝑟, 𝑠〉 = 〈𝑥, 𝑦〉)) |
14 | | opeq1 4340 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 〈𝑟, 𝑠〉 → 〈𝑎, 𝑡〉 = 〈〈𝑟, 𝑠〉, 𝑡〉) |
15 | 14 | eqeq2d 2620 |
. . . . . . . . . . . 12
⊢ (𝑎 = 〈𝑟, 𝑠〉 → (𝑤 = 〈𝑎, 𝑡〉 ↔ 𝑤 = 〈〈𝑟, 𝑠〉, 𝑡〉)) |
16 | 11, 12, 3 | otth2 4878 |
. . . . . . . . . . . . . . . . . . 19
⊢
(〈〈𝑥,
𝑦〉, 𝑧〉 = 〈〈𝑟, 𝑠〉, 𝑡〉 ↔ (𝑥 = 𝑟 ∧ 𝑦 = 𝑠 ∧ 𝑧 = 𝑡)) |
17 | | df-3an 1033 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 = 𝑟 ∧ 𝑦 = 𝑠 ∧ 𝑧 = 𝑡) ↔ ((𝑥 = 𝑟 ∧ 𝑦 = 𝑠) ∧ 𝑧 = 𝑡)) |
18 | 16, 17 | bitri 263 |
. . . . . . . . . . . . . . . . . 18
⊢
(〈〈𝑥,
𝑦〉, 𝑧〉 = 〈〈𝑟, 𝑠〉, 𝑡〉 ↔ ((𝑥 = 𝑟 ∧ 𝑦 = 𝑠) ∧ 𝑧 = 𝑡)) |
19 | 18 | anbi1i 727 |
. . . . . . . . . . . . . . . . 17
⊢
((〈〈𝑥,
𝑦〉, 𝑧〉 = 〈〈𝑟, 𝑠〉, 𝑡〉 ∧ 𝜑) ↔ (((𝑥 = 𝑟 ∧ 𝑦 = 𝑠) ∧ 𝑧 = 𝑡) ∧ 𝜑)) |
20 | | anass 679 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑥 = 𝑟 ∧ 𝑦 = 𝑠) ∧ 𝑧 = 𝑡) ∧ 𝜑) ↔ ((𝑥 = 𝑟 ∧ 𝑦 = 𝑠) ∧ (𝑧 = 𝑡 ∧ 𝜑))) |
21 | | anass 679 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 = 𝑟 ∧ 𝑦 = 𝑠) ∧ (𝑧 = 𝑡 ∧ 𝜑)) ↔ (𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑)))) |
22 | 19, 20, 21 | 3bitri 285 |
. . . . . . . . . . . . . . . 16
⊢
((〈〈𝑥,
𝑦〉, 𝑧〉 = 〈〈𝑟, 𝑠〉, 𝑡〉 ∧ 𝜑) ↔ (𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑)))) |
23 | 22 | 3exbii 1766 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑥∃𝑦∃𝑧(〈〈𝑥, 𝑦〉, 𝑧〉 = 〈〈𝑟, 𝑠〉, 𝑡〉 ∧ 𝜑) ↔ ∃𝑥∃𝑦∃𝑧(𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑)))) |
24 | | nfcvf2 2775 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (¬
∀𝑥 𝑥 = 𝑧 → Ⅎ𝑧𝑥) |
25 | | nfcvd 2752 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (¬
∀𝑥 𝑥 = 𝑧 → Ⅎ𝑧𝑟) |
26 | 24, 25 | nfeqd 2758 |
. . . . . . . . . . . . . . . . . . 19
⊢ (¬
∀𝑥 𝑥 = 𝑧 → Ⅎ𝑧 𝑥 = 𝑟) |
27 | 26 | exdistrf 2321 |
. . . . . . . . . . . . . . . . . 18
⊢
(∃𝑥∃𝑧(𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) → ∃𝑥(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑)))) |
28 | 27 | eximi 1752 |
. . . . . . . . . . . . . . . . 17
⊢
(∃𝑦∃𝑥∃𝑧(𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) → ∃𝑦∃𝑥(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑)))) |
29 | | excom 2029 |
. . . . . . . . . . . . . . . . 17
⊢
(∃𝑥∃𝑦∃𝑧(𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) ↔ ∃𝑦∃𝑥∃𝑧(𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑)))) |
30 | | excom 2029 |
. . . . . . . . . . . . . . . . 17
⊢
(∃𝑥∃𝑦(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) ↔ ∃𝑦∃𝑥(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑)))) |
31 | 28, 29, 30 | 3imtr4i 280 |
. . . . . . . . . . . . . . . 16
⊢
(∃𝑥∃𝑦∃𝑧(𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) → ∃𝑥∃𝑦(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑)))) |
32 | | nfcvf2 2775 |
. . . . . . . . . . . . . . . . . 18
⊢ (¬
∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦𝑥) |
33 | | nfcvd 2752 |
. . . . . . . . . . . . . . . . . 18
⊢ (¬
∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦𝑟) |
34 | 32, 33 | nfeqd 2758 |
. . . . . . . . . . . . . . . . 17
⊢ (¬
∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦 𝑥 = 𝑟) |
35 | 34 | exdistrf 2321 |
. . . . . . . . . . . . . . . 16
⊢
(∃𝑥∃𝑦(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) → ∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑)))) |
36 | | nfcvf2 2775 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (¬
∀𝑦 𝑦 = 𝑧 → Ⅎ𝑧𝑦) |
37 | | nfcvd 2752 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (¬
∀𝑦 𝑦 = 𝑧 → Ⅎ𝑧𝑠) |
38 | 36, 37 | nfeqd 2758 |
. . . . . . . . . . . . . . . . . . 19
⊢ (¬
∀𝑦 𝑦 = 𝑧 → Ⅎ𝑧 𝑦 = 𝑠) |
39 | 38 | exdistrf 2321 |
. . . . . . . . . . . . . . . . . 18
⊢
(∃𝑦∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑)) → ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑))) |
40 | 39 | anim2i 591 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 = 𝑟 ∧ ∃𝑦∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) → (𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑)))) |
41 | 40 | eximi 1752 |
. . . . . . . . . . . . . . . 16
⊢
(∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) → ∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑)))) |
42 | 31, 35, 41 | 3syl 18 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑥∃𝑦∃𝑧(𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) → ∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑)))) |
43 | 23, 42 | sylbi 206 |
. . . . . . . . . . . . . 14
⊢
(∃𝑥∃𝑦∃𝑧(〈〈𝑥, 𝑦〉, 𝑧〉 = 〈〈𝑟, 𝑠〉, 𝑡〉 ∧ 𝜑) → ∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑)))) |
44 | | euequ1 2464 |
. . . . . . . . . . . . . . . . . . 19
⊢
∃!𝑥 𝑥 = 𝑟 |
45 | | eupick 2524 |
. . . . . . . . . . . . . . . . . . 19
⊢
((∃!𝑥 𝑥 = 𝑟 ∧ ∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑)))) → (𝑥 = 𝑟 → ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑)))) |
46 | 44, 45 | mpan 702 |
. . . . . . . . . . . . . . . . . 18
⊢
(∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑))) → (𝑥 = 𝑟 → ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑)))) |
47 | | euequ1 2464 |
. . . . . . . . . . . . . . . . . . . 20
⊢
∃!𝑦 𝑦 = 𝑠 |
48 | | eupick 2524 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((∃!𝑦 𝑦 = 𝑠 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑))) → (𝑦 = 𝑠 → ∃𝑧(𝑧 = 𝑡 ∧ 𝜑))) |
49 | 47, 48 | mpan 702 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑)) → (𝑦 = 𝑠 → ∃𝑧(𝑧 = 𝑡 ∧ 𝜑))) |
50 | | euequ1 2464 |
. . . . . . . . . . . . . . . . . . . 20
⊢
∃!𝑧 𝑧 = 𝑡 |
51 | | eupick 2524 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((∃!𝑧 𝑧 = 𝑡 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑)) → (𝑧 = 𝑡 → 𝜑)) |
52 | 50, 51 | mpan 702 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∃𝑧(𝑧 = 𝑡 ∧ 𝜑) → (𝑧 = 𝑡 → 𝜑)) |
53 | 49, 52 | syl6 34 |
. . . . . . . . . . . . . . . . . 18
⊢
(∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑)) → (𝑦 = 𝑠 → (𝑧 = 𝑡 → 𝜑))) |
54 | 46, 53 | syl6 34 |
. . . . . . . . . . . . . . . . 17
⊢
(∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑))) → (𝑥 = 𝑟 → (𝑦 = 𝑠 → (𝑧 = 𝑡 → 𝜑)))) |
55 | 54 | 3impd 1273 |
. . . . . . . . . . . . . . . 16
⊢
(∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑))) → ((𝑥 = 𝑟 ∧ 𝑦 = 𝑠 ∧ 𝑧 = 𝑡) → 𝜑)) |
56 | 16, 55 | syl5bi 231 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑))) → (〈〈𝑥, 𝑦〉, 𝑧〉 = 〈〈𝑟, 𝑠〉, 𝑡〉 → 𝜑)) |
57 | 56 | com12 32 |
. . . . . . . . . . . . . 14
⊢
(〈〈𝑥,
𝑦〉, 𝑧〉 = 〈〈𝑟, 𝑠〉, 𝑡〉 → (∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑))) → 𝜑)) |
58 | 43, 57 | syl5 33 |
. . . . . . . . . . . . 13
⊢
(〈〈𝑥,
𝑦〉, 𝑧〉 = 〈〈𝑟, 𝑠〉, 𝑡〉 → (∃𝑥∃𝑦∃𝑧(〈〈𝑥, 𝑦〉, 𝑧〉 = 〈〈𝑟, 𝑠〉, 𝑡〉 ∧ 𝜑) → 𝜑)) |
59 | | eqeq1 2614 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = 〈〈𝑟, 𝑠〉, 𝑡〉 → (𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ↔ 〈〈𝑟, 𝑠〉, 𝑡〉 = 〈〈𝑥, 𝑦〉, 𝑧〉)) |
60 | | eqcom 2617 |
. . . . . . . . . . . . . . 15
⊢
(〈〈𝑟,
𝑠〉, 𝑡〉 = 〈〈𝑥, 𝑦〉, 𝑧〉 ↔ 〈〈𝑥, 𝑦〉, 𝑧〉 = 〈〈𝑟, 𝑠〉, 𝑡〉) |
61 | 59, 60 | syl6bb 275 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = 〈〈𝑟, 𝑠〉, 𝑡〉 → (𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ↔ 〈〈𝑥, 𝑦〉, 𝑧〉 = 〈〈𝑟, 𝑠〉, 𝑡〉)) |
62 | 61 | anbi1d 737 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = 〈〈𝑟, 𝑠〉, 𝑡〉 → ((𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) ↔ (〈〈𝑥, 𝑦〉, 𝑧〉 = 〈〈𝑟, 𝑠〉, 𝑡〉 ∧ 𝜑))) |
63 | 62 | 3exbidv 1840 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = 〈〈𝑟, 𝑠〉, 𝑡〉 → (∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) ↔ ∃𝑥∃𝑦∃𝑧(〈〈𝑥, 𝑦〉, 𝑧〉 = 〈〈𝑟, 𝑠〉, 𝑡〉 ∧ 𝜑))) |
64 | 63 | imbi1d 330 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = 〈〈𝑟, 𝑠〉, 𝑡〉 → ((∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) → 𝜑) ↔ (∃𝑥∃𝑦∃𝑧(〈〈𝑥, 𝑦〉, 𝑧〉 = 〈〈𝑟, 𝑠〉, 𝑡〉 ∧ 𝜑) → 𝜑))) |
65 | 61, 64 | imbi12d 333 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 〈〈𝑟, 𝑠〉, 𝑡〉 → ((𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 → (∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) → 𝜑)) ↔ (〈〈𝑥, 𝑦〉, 𝑧〉 = 〈〈𝑟, 𝑠〉, 𝑡〉 → (∃𝑥∃𝑦∃𝑧(〈〈𝑥, 𝑦〉, 𝑧〉 = 〈〈𝑟, 𝑠〉, 𝑡〉 ∧ 𝜑) → 𝜑)))) |
66 | 58, 65 | mpbiri 247 |
. . . . . . . . . . . 12
⊢ (𝑤 = 〈〈𝑟, 𝑠〉, 𝑡〉 → (𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 → (∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) → 𝜑))) |
67 | 15, 66 | syl6bi 242 |
. . . . . . . . . . 11
⊢ (𝑎 = 〈𝑟, 𝑠〉 → (𝑤 = 〈𝑎, 𝑡〉 → (𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 → (∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) → 𝜑)))) |
68 | 67 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑎 = 〈𝑟, 𝑠〉 ∧ 〈𝑟, 𝑠〉 = 〈𝑥, 𝑦〉) → (𝑤 = 〈𝑎, 𝑡〉 → (𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 → (∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) → 𝜑)))) |
69 | 68 | exlimivv 1847 |
. . . . . . . . 9
⊢
(∃𝑟∃𝑠(𝑎 = 〈𝑟, 𝑠〉 ∧ 〈𝑟, 𝑠〉 = 〈𝑥, 𝑦〉) → (𝑤 = 〈𝑎, 𝑡〉 → (𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 → (∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) → 𝜑)))) |
70 | 13, 69 | sylbi 206 |
. . . . . . . 8
⊢ (𝑎 = 〈𝑥, 𝑦〉 → (𝑤 = 〈𝑎, 𝑡〉 → (𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 → (∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) → 𝜑)))) |
71 | 70 | com3l 87 |
. . . . . . 7
⊢ (𝑤 = 〈𝑎, 𝑡〉 → (𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 → (𝑎 = 〈𝑥, 𝑦〉 → (∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) → 𝜑)))) |
72 | 10, 71 | mpdd 42 |
. . . . . 6
⊢ (𝑤 = 〈𝑎, 𝑡〉 → (𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 → (∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) → 𝜑))) |
73 | 72 | adantr 480 |
. . . . 5
⊢ ((𝑤 = 〈𝑎, 𝑡〉 ∧ 〈𝑎, 𝑡〉 = 〈〈𝑥, 𝑦〉, 𝑧〉) → (𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 → (∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) → 𝜑))) |
74 | 73 | exlimivv 1847 |
. . . 4
⊢
(∃𝑎∃𝑡(𝑤 = 〈𝑎, 𝑡〉 ∧ 〈𝑎, 𝑡〉 = 〈〈𝑥, 𝑦〉, 𝑧〉) → (𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 → (∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) → 𝜑))) |
75 | 5, 74 | mpcom 37 |
. . 3
⊢ (𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 → (∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) → 𝜑)) |
76 | | 19.8a 2039 |
. . . . 5
⊢ ((𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) → ∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑)) |
77 | | 19.8a 2039 |
. . . . 5
⊢
(∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) → ∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑)) |
78 | | 19.8a 2039 |
. . . . 5
⊢
(∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) → ∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑)) |
79 | 76, 77, 78 | 3syl 18 |
. . . 4
⊢ ((𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) → ∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑)) |
80 | 79 | ex 449 |
. . 3
⊢ (𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 → (𝜑 → ∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑))) |
81 | 75, 80 | impbid 201 |
. 2
⊢ (𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 → (∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑) ↔ 𝜑)) |
82 | | df-oprab 6553 |
. 2
⊢
{〈〈𝑥,
𝑦〉, 𝑧〉 ∣ 𝜑} = {𝑤 ∣ ∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑)} |
83 | 1, 81, 82 | elab2 3323 |
1
⊢
(〈〈𝑥,
𝑦〉, 𝑧〉 ∈ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} ↔ 𝜑) |