Step | Hyp | Ref
| Expression |
1 | | vex 3434 |
. . . 4
⊢ 𝑥 ∈ V |
2 | | vex 3434 |
. . . 4
⊢ 𝑦 ∈ V |
3 | 1, 2 | eqvinop 5403 |
. . 3
⊢ (𝐴 = 〈𝑥, 𝑦〉 ↔ ∃𝑧∃𝑤(𝐴 = 〈𝑧, 𝑤〉 ∧ 〈𝑧, 𝑤〉 = 〈𝑥, 𝑦〉)) |
4 | | 19.8a 2177 |
. . . . . . . . 9
⊢
(∃𝑦(〈𝑧, 𝑤〉 = 〈𝑥, 𝑦〉 ∧ 𝜑) → ∃𝑥∃𝑦(〈𝑧, 𝑤〉 = 〈𝑥, 𝑦〉 ∧ 𝜑)) |
5 | 4 | 19.23bi 2187 |
. . . . . . . 8
⊢
((〈𝑧, 𝑤〉 = 〈𝑥, 𝑦〉 ∧ 𝜑) → ∃𝑥∃𝑦(〈𝑧, 𝑤〉 = 〈𝑥, 𝑦〉 ∧ 𝜑)) |
6 | 5 | ex 412 |
. . . . . . 7
⊢
(〈𝑧, 𝑤〉 = 〈𝑥, 𝑦〉 → (𝜑 → ∃𝑥∃𝑦(〈𝑧, 𝑤〉 = 〈𝑥, 𝑦〉 ∧ 𝜑))) |
7 | | vex 3434 |
. . . . . . . . 9
⊢ 𝑧 ∈ V |
8 | | vex 3434 |
. . . . . . . . 9
⊢ 𝑤 ∈ V |
9 | 7, 8 | opth 5393 |
. . . . . . . 8
⊢
(〈𝑧, 𝑤〉 = 〈𝑥, 𝑦〉 ↔ (𝑧 = 𝑥 ∧ 𝑤 = 𝑦)) |
10 | 9 | anbi1i 623 |
. . . . . . . . . 10
⊢
((〈𝑧, 𝑤〉 = 〈𝑥, 𝑦〉 ∧ 𝜑) ↔ ((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) ∧ 𝜑)) |
11 | 10 | 2exbii 1854 |
. . . . . . . . 9
⊢
(∃𝑥∃𝑦(〈𝑧, 𝑤〉 = 〈𝑥, 𝑦〉 ∧ 𝜑) ↔ ∃𝑥∃𝑦((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) ∧ 𝜑)) |
12 | | nfe1 2150 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥∃𝑥(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦 ∧ 𝜑)) |
13 | | 19.8a 2177 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑤 = 𝑦 ∧ 𝜑) → ∃𝑦(𝑤 = 𝑦 ∧ 𝜑)) |
14 | 13 | anim2i 616 |
. . . . . . . . . . . . . . 15
⊢ ((𝑧 = 𝑥 ∧ (𝑤 = 𝑦 ∧ 𝜑)) → (𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦 ∧ 𝜑))) |
15 | 14 | anassrs 467 |
. . . . . . . . . . . . . 14
⊢ (((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) ∧ 𝜑) → (𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦 ∧ 𝜑))) |
16 | 15 | eximi 1840 |
. . . . . . . . . . . . 13
⊢
(∃𝑦((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) ∧ 𝜑) → ∃𝑦(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦 ∧ 𝜑))) |
17 | | biidd 261 |
. . . . . . . . . . . . . 14
⊢
(∀𝑦 𝑦 = 𝑥 → ((𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦 ∧ 𝜑)) ↔ (𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦 ∧ 𝜑)))) |
18 | 17 | drex1 2442 |
. . . . . . . . . . . . 13
⊢
(∀𝑦 𝑦 = 𝑥 → (∃𝑦(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦 ∧ 𝜑)) ↔ ∃𝑥(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦 ∧ 𝜑)))) |
19 | 16, 18 | syl5ib 243 |
. . . . . . . . . . . 12
⊢
(∀𝑦 𝑦 = 𝑥 → (∃𝑦((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) ∧ 𝜑) → ∃𝑥(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦 ∧ 𝜑)))) |
20 | | anass 468 |
. . . . . . . . . . . . . . 15
⊢ (((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) ∧ 𝜑) ↔ (𝑧 = 𝑥 ∧ (𝑤 = 𝑦 ∧ 𝜑))) |
21 | 20 | exbii 1853 |
. . . . . . . . . . . . . 14
⊢
(∃𝑦((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) ∧ 𝜑) ↔ ∃𝑦(𝑧 = 𝑥 ∧ (𝑤 = 𝑦 ∧ 𝜑))) |
22 | | 19.40 1892 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑦(𝑧 = 𝑥 ∧ (𝑤 = 𝑦 ∧ 𝜑)) → (∃𝑦 𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦 ∧ 𝜑))) |
23 | | nfeqf2 2378 |
. . . . . . . . . . . . . . . . 17
⊢ (¬
∀𝑦 𝑦 = 𝑥 → Ⅎ𝑦 𝑧 = 𝑥) |
24 | 23 | 19.9d 2199 |
. . . . . . . . . . . . . . . 16
⊢ (¬
∀𝑦 𝑦 = 𝑥 → (∃𝑦 𝑧 = 𝑥 → 𝑧 = 𝑥)) |
25 | 24 | anim1d 610 |
. . . . . . . . . . . . . . 15
⊢ (¬
∀𝑦 𝑦 = 𝑥 → ((∃𝑦 𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦 ∧ 𝜑)) → (𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦 ∧ 𝜑)))) |
26 | 22, 25 | syl5 34 |
. . . . . . . . . . . . . 14
⊢ (¬
∀𝑦 𝑦 = 𝑥 → (∃𝑦(𝑧 = 𝑥 ∧ (𝑤 = 𝑦 ∧ 𝜑)) → (𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦 ∧ 𝜑)))) |
27 | 21, 26 | syl5bi 241 |
. . . . . . . . . . . . 13
⊢ (¬
∀𝑦 𝑦 = 𝑥 → (∃𝑦((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) ∧ 𝜑) → (𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦 ∧ 𝜑)))) |
28 | | 19.8a 2177 |
. . . . . . . . . . . . 13
⊢ ((𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦 ∧ 𝜑)) → ∃𝑥(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦 ∧ 𝜑))) |
29 | 27, 28 | syl6 35 |
. . . . . . . . . . . 12
⊢ (¬
∀𝑦 𝑦 = 𝑥 → (∃𝑦((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) ∧ 𝜑) → ∃𝑥(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦 ∧ 𝜑)))) |
30 | 19, 29 | pm2.61i 182 |
. . . . . . . . . . 11
⊢
(∃𝑦((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) ∧ 𝜑) → ∃𝑥(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦 ∧ 𝜑))) |
31 | 12, 30 | exlimi 2213 |
. . . . . . . . . 10
⊢
(∃𝑥∃𝑦((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) ∧ 𝜑) → ∃𝑥(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦 ∧ 𝜑))) |
32 | | euequ 2598 |
. . . . . . . . . . . . . 14
⊢
∃!𝑥 𝑥 = 𝑧 |
33 | | equcom 2024 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑧 ↔ 𝑧 = 𝑥) |
34 | 33 | eubii 2586 |
. . . . . . . . . . . . . 14
⊢
(∃!𝑥 𝑥 = 𝑧 ↔ ∃!𝑥 𝑧 = 𝑥) |
35 | 32, 34 | mpbi 229 |
. . . . . . . . . . . . 13
⊢
∃!𝑥 𝑧 = 𝑥 |
36 | | eupick 2636 |
. . . . . . . . . . . . 13
⊢
((∃!𝑥 𝑧 = 𝑥 ∧ ∃𝑥(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦 ∧ 𝜑))) → (𝑧 = 𝑥 → ∃𝑦(𝑤 = 𝑦 ∧ 𝜑))) |
37 | 35, 36 | mpan 686 |
. . . . . . . . . . . 12
⊢
(∃𝑥(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦 ∧ 𝜑)) → (𝑧 = 𝑥 → ∃𝑦(𝑤 = 𝑦 ∧ 𝜑))) |
38 | 37 | com12 32 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑥 → (∃𝑥(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦 ∧ 𝜑)) → ∃𝑦(𝑤 = 𝑦 ∧ 𝜑))) |
39 | | euequ 2598 |
. . . . . . . . . . . . . 14
⊢
∃!𝑦 𝑦 = 𝑤 |
40 | | equcom 2024 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑤 ↔ 𝑤 = 𝑦) |
41 | 40 | eubii 2586 |
. . . . . . . . . . . . . 14
⊢
(∃!𝑦 𝑦 = 𝑤 ↔ ∃!𝑦 𝑤 = 𝑦) |
42 | 39, 41 | mpbi 229 |
. . . . . . . . . . . . 13
⊢
∃!𝑦 𝑤 = 𝑦 |
43 | | eupick 2636 |
. . . . . . . . . . . . 13
⊢
((∃!𝑦 𝑤 = 𝑦 ∧ ∃𝑦(𝑤 = 𝑦 ∧ 𝜑)) → (𝑤 = 𝑦 → 𝜑)) |
44 | 42, 43 | mpan 686 |
. . . . . . . . . . . 12
⊢
(∃𝑦(𝑤 = 𝑦 ∧ 𝜑) → (𝑤 = 𝑦 → 𝜑)) |
45 | 44 | com12 32 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑦 → (∃𝑦(𝑤 = 𝑦 ∧ 𝜑) → 𝜑)) |
46 | 38, 45 | sylan9 507 |
. . . . . . . . . 10
⊢ ((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) → (∃𝑥(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦 ∧ 𝜑)) → 𝜑)) |
47 | 31, 46 | syl5 34 |
. . . . . . . . 9
⊢ ((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) → (∃𝑥∃𝑦((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) ∧ 𝜑) → 𝜑)) |
48 | 11, 47 | syl5bi 241 |
. . . . . . . 8
⊢ ((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) → (∃𝑥∃𝑦(〈𝑧, 𝑤〉 = 〈𝑥, 𝑦〉 ∧ 𝜑) → 𝜑)) |
49 | 9, 48 | sylbi 216 |
. . . . . . 7
⊢
(〈𝑧, 𝑤〉 = 〈𝑥, 𝑦〉 → (∃𝑥∃𝑦(〈𝑧, 𝑤〉 = 〈𝑥, 𝑦〉 ∧ 𝜑) → 𝜑)) |
50 | 6, 49 | impbid 211 |
. . . . . 6
⊢
(〈𝑧, 𝑤〉 = 〈𝑥, 𝑦〉 → (𝜑 ↔ ∃𝑥∃𝑦(〈𝑧, 𝑤〉 = 〈𝑥, 𝑦〉 ∧ 𝜑))) |
51 | | eqeq1 2743 |
. . . . . . 7
⊢ (𝐴 = 〈𝑧, 𝑤〉 → (𝐴 = 〈𝑥, 𝑦〉 ↔ 〈𝑧, 𝑤〉 = 〈𝑥, 𝑦〉)) |
52 | 51 | anbi1d 629 |
. . . . . . . . 9
⊢ (𝐴 = 〈𝑧, 𝑤〉 → ((𝐴 = 〈𝑥, 𝑦〉 ∧ 𝜑) ↔ (〈𝑧, 𝑤〉 = 〈𝑥, 𝑦〉 ∧ 𝜑))) |
53 | 52 | 2exbidv 1930 |
. . . . . . . 8
⊢ (𝐴 = 〈𝑧, 𝑤〉 → (∃𝑥∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ 𝜑) ↔ ∃𝑥∃𝑦(〈𝑧, 𝑤〉 = 〈𝑥, 𝑦〉 ∧ 𝜑))) |
54 | 53 | bibi2d 342 |
. . . . . . 7
⊢ (𝐴 = 〈𝑧, 𝑤〉 → ((𝜑 ↔ ∃𝑥∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ 𝜑)) ↔ (𝜑 ↔ ∃𝑥∃𝑦(〈𝑧, 𝑤〉 = 〈𝑥, 𝑦〉 ∧ 𝜑)))) |
55 | 51, 54 | imbi12d 344 |
. . . . . 6
⊢ (𝐴 = 〈𝑧, 𝑤〉 → ((𝐴 = 〈𝑥, 𝑦〉 → (𝜑 ↔ ∃𝑥∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ 𝜑))) ↔ (〈𝑧, 𝑤〉 = 〈𝑥, 𝑦〉 → (𝜑 ↔ ∃𝑥∃𝑦(〈𝑧, 𝑤〉 = 〈𝑥, 𝑦〉 ∧ 𝜑))))) |
56 | 50, 55 | mpbiri 257 |
. . . . 5
⊢ (𝐴 = 〈𝑧, 𝑤〉 → (𝐴 = 〈𝑥, 𝑦〉 → (𝜑 ↔ ∃𝑥∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ 𝜑)))) |
57 | 56 | adantr 480 |
. . . 4
⊢ ((𝐴 = 〈𝑧, 𝑤〉 ∧ 〈𝑧, 𝑤〉 = 〈𝑥, 𝑦〉) → (𝐴 = 〈𝑥, 𝑦〉 → (𝜑 ↔ ∃𝑥∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ 𝜑)))) |
58 | 57 | exlimivv 1938 |
. . 3
⊢
(∃𝑧∃𝑤(𝐴 = 〈𝑧, 𝑤〉 ∧ 〈𝑧, 𝑤〉 = 〈𝑥, 𝑦〉) → (𝐴 = 〈𝑥, 𝑦〉 → (𝜑 ↔ ∃𝑥∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ 𝜑)))) |
59 | 3, 58 | sylbi 216 |
. 2
⊢ (𝐴 = 〈𝑥, 𝑦〉 → (𝐴 = 〈𝑥, 𝑦〉 → (𝜑 ↔ ∃𝑥∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ 𝜑)))) |
60 | 59 | pm2.43i 52 |
1
⊢ (𝐴 = 〈𝑥, 𝑦〉 → (𝜑 ↔ ∃𝑥∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ 𝜑))) |