Step | Hyp | Ref
| Expression |
1 | | vex 2738 |
. . . 4
⊢ 𝑥 ∈ V |
2 | | vex 2738 |
. . . 4
⊢ 𝑦 ∈ V |
3 | 1, 2 | eqvinop 4237 |
. . 3
⊢ (𝐴 = 〈𝑥, 𝑦〉 ↔ ∃𝑧∃𝑤(𝐴 = 〈𝑧, 𝑤〉 ∧ 〈𝑧, 𝑤〉 = 〈𝑥, 𝑦〉)) |
4 | | 19.8a 1588 |
. . . . . . . . 9
⊢
(∃𝑦(〈𝑧, 𝑤〉 = 〈𝑥, 𝑦〉 ∧ 𝜑) → ∃𝑥∃𝑦(〈𝑧, 𝑤〉 = 〈𝑥, 𝑦〉 ∧ 𝜑)) |
5 | 4 | 19.23bi 1590 |
. . . . . . . 8
⊢
((〈𝑧, 𝑤〉 = 〈𝑥, 𝑦〉 ∧ 𝜑) → ∃𝑥∃𝑦(〈𝑧, 𝑤〉 = 〈𝑥, 𝑦〉 ∧ 𝜑)) |
6 | 5 | ex 115 |
. . . . . . 7
⊢
(〈𝑧, 𝑤〉 = 〈𝑥, 𝑦〉 → (𝜑 → ∃𝑥∃𝑦(〈𝑧, 𝑤〉 = 〈𝑥, 𝑦〉 ∧ 𝜑))) |
7 | | vex 2738 |
. . . . . . . . 9
⊢ 𝑧 ∈ V |
8 | | vex 2738 |
. . . . . . . . 9
⊢ 𝑤 ∈ V |
9 | 7, 8 | opth 4231 |
. . . . . . . 8
⊢
(〈𝑧, 𝑤〉 = 〈𝑥, 𝑦〉 ↔ (𝑧 = 𝑥 ∧ 𝑤 = 𝑦)) |
10 | 9 | anbi1i 458 |
. . . . . . . . . 10
⊢
((〈𝑧, 𝑤〉 = 〈𝑥, 𝑦〉 ∧ 𝜑) ↔ ((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) ∧ 𝜑)) |
11 | 10 | 2exbii 1604 |
. . . . . . . . 9
⊢
(∃𝑥∃𝑦(〈𝑧, 𝑤〉 = 〈𝑥, 𝑦〉 ∧ 𝜑) ↔ ∃𝑥∃𝑦((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) ∧ 𝜑)) |
12 | | nfe1 1494 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥∃𝑥(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦 ∧ 𝜑)) |
13 | | dveeq2or 1814 |
. . . . . . . . . . . 12
⊢
(∀𝑦 𝑦 = 𝑥 ∨ Ⅎ𝑦 𝑧 = 𝑥) |
14 | | nfae 1717 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑦∀𝑦 𝑦 = 𝑥 |
15 | | anass 401 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) ∧ 𝜑) ↔ (𝑧 = 𝑥 ∧ (𝑤 = 𝑦 ∧ 𝜑))) |
16 | | 19.8a 1588 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑤 = 𝑦 ∧ 𝜑) → ∃𝑦(𝑤 = 𝑦 ∧ 𝜑)) |
17 | 16 | a1i 9 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑦 𝑦 = 𝑥 → ((𝑤 = 𝑦 ∧ 𝜑) → ∃𝑦(𝑤 = 𝑦 ∧ 𝜑))) |
18 | 17 | anim2d 337 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑦 𝑦 = 𝑥 → ((𝑧 = 𝑥 ∧ (𝑤 = 𝑦 ∧ 𝜑)) → (𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦 ∧ 𝜑)))) |
19 | 15, 18 | biimtrid 152 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑦 𝑦 = 𝑥 → (((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) ∧ 𝜑) → (𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦 ∧ 𝜑)))) |
20 | 14, 19 | eximd 1610 |
. . . . . . . . . . . . . 14
⊢
(∀𝑦 𝑦 = 𝑥 → (∃𝑦((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) ∧ 𝜑) → ∃𝑦(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦 ∧ 𝜑)))) |
21 | | biidd 172 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑦 𝑦 = 𝑥 → ((𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦 ∧ 𝜑)) ↔ (𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦 ∧ 𝜑)))) |
22 | 21 | drex1 1796 |
. . . . . . . . . . . . . 14
⊢
(∀𝑦 𝑦 = 𝑥 → (∃𝑦(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦 ∧ 𝜑)) ↔ ∃𝑥(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦 ∧ 𝜑)))) |
23 | 20, 22 | sylibd 149 |
. . . . . . . . . . . . 13
⊢
(∀𝑦 𝑦 = 𝑥 → (∃𝑦((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) ∧ 𝜑) → ∃𝑥(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦 ∧ 𝜑)))) |
24 | 15 | exbii 1603 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑦((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) ∧ 𝜑) ↔ ∃𝑦(𝑧 = 𝑥 ∧ (𝑤 = 𝑦 ∧ 𝜑))) |
25 | | 19.40 1629 |
. . . . . . . . . . . . . . . 16
⊢
(∃𝑦(𝑧 = 𝑥 ∧ (𝑤 = 𝑦 ∧ 𝜑)) → (∃𝑦 𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦 ∧ 𝜑))) |
26 | | 19.9t 1640 |
. . . . . . . . . . . . . . . . . 18
⊢
(Ⅎ𝑦 𝑧 = 𝑥 → (∃𝑦 𝑧 = 𝑥 ↔ 𝑧 = 𝑥)) |
27 | 26 | biimpd 144 |
. . . . . . . . . . . . . . . . 17
⊢
(Ⅎ𝑦 𝑧 = 𝑥 → (∃𝑦 𝑧 = 𝑥 → 𝑧 = 𝑥)) |
28 | 27 | anim1d 336 |
. . . . . . . . . . . . . . . 16
⊢
(Ⅎ𝑦 𝑧 = 𝑥 → ((∃𝑦 𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦 ∧ 𝜑)) → (𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦 ∧ 𝜑)))) |
29 | 25, 28 | syl5 32 |
. . . . . . . . . . . . . . 15
⊢
(Ⅎ𝑦 𝑧 = 𝑥 → (∃𝑦(𝑧 = 𝑥 ∧ (𝑤 = 𝑦 ∧ 𝜑)) → (𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦 ∧ 𝜑)))) |
30 | 24, 29 | biimtrid 152 |
. . . . . . . . . . . . . 14
⊢
(Ⅎ𝑦 𝑧 = 𝑥 → (∃𝑦((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) ∧ 𝜑) → (𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦 ∧ 𝜑)))) |
31 | | 19.8a 1588 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦 ∧ 𝜑)) → ∃𝑥(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦 ∧ 𝜑))) |
32 | 30, 31 | syl6 33 |
. . . . . . . . . . . . 13
⊢
(Ⅎ𝑦 𝑧 = 𝑥 → (∃𝑦((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) ∧ 𝜑) → ∃𝑥(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦 ∧ 𝜑)))) |
33 | 23, 32 | jaoi 716 |
. . . . . . . . . . . 12
⊢
((∀𝑦 𝑦 = 𝑥 ∨ Ⅎ𝑦 𝑧 = 𝑥) → (∃𝑦((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) ∧ 𝜑) → ∃𝑥(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦 ∧ 𝜑)))) |
34 | 13, 33 | ax-mp 5 |
. . . . . . . . . . 11
⊢
(∃𝑦((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) ∧ 𝜑) → ∃𝑥(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦 ∧ 𝜑))) |
35 | 12, 34 | exlimi 1592 |
. . . . . . . . . 10
⊢
(∃𝑥∃𝑦((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) ∧ 𝜑) → ∃𝑥(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦 ∧ 𝜑))) |
36 | | euequ1 2119 |
. . . . . . . . . . . . . 14
⊢
∃!𝑥 𝑥 = 𝑧 |
37 | | equcom 1704 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑧 ↔ 𝑧 = 𝑥) |
38 | 37 | eubii 2033 |
. . . . . . . . . . . . . 14
⊢
(∃!𝑥 𝑥 = 𝑧 ↔ ∃!𝑥 𝑧 = 𝑥) |
39 | 36, 38 | mpbi 145 |
. . . . . . . . . . . . 13
⊢
∃!𝑥 𝑧 = 𝑥 |
40 | | eupick 2103 |
. . . . . . . . . . . . 13
⊢
((∃!𝑥 𝑧 = 𝑥 ∧ ∃𝑥(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦 ∧ 𝜑))) → (𝑧 = 𝑥 → ∃𝑦(𝑤 = 𝑦 ∧ 𝜑))) |
41 | 39, 40 | mpan 424 |
. . . . . . . . . . . 12
⊢
(∃𝑥(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦 ∧ 𝜑)) → (𝑧 = 𝑥 → ∃𝑦(𝑤 = 𝑦 ∧ 𝜑))) |
42 | 41 | com12 30 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑥 → (∃𝑥(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦 ∧ 𝜑)) → ∃𝑦(𝑤 = 𝑦 ∧ 𝜑))) |
43 | | euequ1 2119 |
. . . . . . . . . . . . . 14
⊢
∃!𝑦 𝑦 = 𝑤 |
44 | | equcom 1704 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑤 ↔ 𝑤 = 𝑦) |
45 | 44 | eubii 2033 |
. . . . . . . . . . . . . 14
⊢
(∃!𝑦 𝑦 = 𝑤 ↔ ∃!𝑦 𝑤 = 𝑦) |
46 | 43, 45 | mpbi 145 |
. . . . . . . . . . . . 13
⊢
∃!𝑦 𝑤 = 𝑦 |
47 | | eupick 2103 |
. . . . . . . . . . . . 13
⊢
((∃!𝑦 𝑤 = 𝑦 ∧ ∃𝑦(𝑤 = 𝑦 ∧ 𝜑)) → (𝑤 = 𝑦 → 𝜑)) |
48 | 46, 47 | mpan 424 |
. . . . . . . . . . . 12
⊢
(∃𝑦(𝑤 = 𝑦 ∧ 𝜑) → (𝑤 = 𝑦 → 𝜑)) |
49 | 48 | com12 30 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑦 → (∃𝑦(𝑤 = 𝑦 ∧ 𝜑) → 𝜑)) |
50 | 42, 49 | sylan9 409 |
. . . . . . . . . 10
⊢ ((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) → (∃𝑥(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦 ∧ 𝜑)) → 𝜑)) |
51 | 35, 50 | syl5 32 |
. . . . . . . . 9
⊢ ((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) → (∃𝑥∃𝑦((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) ∧ 𝜑) → 𝜑)) |
52 | 11, 51 | biimtrid 152 |
. . . . . . . 8
⊢ ((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) → (∃𝑥∃𝑦(〈𝑧, 𝑤〉 = 〈𝑥, 𝑦〉 ∧ 𝜑) → 𝜑)) |
53 | 9, 52 | sylbi 121 |
. . . . . . 7
⊢
(〈𝑧, 𝑤〉 = 〈𝑥, 𝑦〉 → (∃𝑥∃𝑦(〈𝑧, 𝑤〉 = 〈𝑥, 𝑦〉 ∧ 𝜑) → 𝜑)) |
54 | 6, 53 | impbid 129 |
. . . . . 6
⊢
(〈𝑧, 𝑤〉 = 〈𝑥, 𝑦〉 → (𝜑 ↔ ∃𝑥∃𝑦(〈𝑧, 𝑤〉 = 〈𝑥, 𝑦〉 ∧ 𝜑))) |
55 | | eqeq1 2182 |
. . . . . . 7
⊢ (𝐴 = 〈𝑧, 𝑤〉 → (𝐴 = 〈𝑥, 𝑦〉 ↔ 〈𝑧, 𝑤〉 = 〈𝑥, 𝑦〉)) |
56 | 55 | anbi1d 465 |
. . . . . . . . 9
⊢ (𝐴 = 〈𝑧, 𝑤〉 → ((𝐴 = 〈𝑥, 𝑦〉 ∧ 𝜑) ↔ (〈𝑧, 𝑤〉 = 〈𝑥, 𝑦〉 ∧ 𝜑))) |
57 | 56 | 2exbidv 1866 |
. . . . . . . 8
⊢ (𝐴 = 〈𝑧, 𝑤〉 → (∃𝑥∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ 𝜑) ↔ ∃𝑥∃𝑦(〈𝑧, 𝑤〉 = 〈𝑥, 𝑦〉 ∧ 𝜑))) |
58 | 57 | bibi2d 232 |
. . . . . . 7
⊢ (𝐴 = 〈𝑧, 𝑤〉 → ((𝜑 ↔ ∃𝑥∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ 𝜑)) ↔ (𝜑 ↔ ∃𝑥∃𝑦(〈𝑧, 𝑤〉 = 〈𝑥, 𝑦〉 ∧ 𝜑)))) |
59 | 55, 58 | imbi12d 234 |
. . . . . 6
⊢ (𝐴 = 〈𝑧, 𝑤〉 → ((𝐴 = 〈𝑥, 𝑦〉 → (𝜑 ↔ ∃𝑥∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ 𝜑))) ↔ (〈𝑧, 𝑤〉 = 〈𝑥, 𝑦〉 → (𝜑 ↔ ∃𝑥∃𝑦(〈𝑧, 𝑤〉 = 〈𝑥, 𝑦〉 ∧ 𝜑))))) |
60 | 54, 59 | mpbiri 168 |
. . . . 5
⊢ (𝐴 = 〈𝑧, 𝑤〉 → (𝐴 = 〈𝑥, 𝑦〉 → (𝜑 ↔ ∃𝑥∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ 𝜑)))) |
61 | 60 | adantr 276 |
. . . 4
⊢ ((𝐴 = 〈𝑧, 𝑤〉 ∧ 〈𝑧, 𝑤〉 = 〈𝑥, 𝑦〉) → (𝐴 = 〈𝑥, 𝑦〉 → (𝜑 ↔ ∃𝑥∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ 𝜑)))) |
62 | 61 | exlimivv 1894 |
. . 3
⊢
(∃𝑧∃𝑤(𝐴 = 〈𝑧, 𝑤〉 ∧ 〈𝑧, 𝑤〉 = 〈𝑥, 𝑦〉) → (𝐴 = 〈𝑥, 𝑦〉 → (𝜑 ↔ ∃𝑥∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ 𝜑)))) |
63 | 3, 62 | sylbi 121 |
. 2
⊢ (𝐴 = 〈𝑥, 𝑦〉 → (𝐴 = 〈𝑥, 𝑦〉 → (𝜑 ↔ ∃𝑥∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ 𝜑)))) |
64 | 63 | pm2.43i 49 |
1
⊢ (𝐴 = 〈𝑥, 𝑦〉 → (𝜑 ↔ ∃𝑥∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ 𝜑))) |