Step | Hyp | Ref
| Expression |
1 | | 19.26 1873 |
. . 3
⊢
(∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤) ↔ (∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤)) |
2 | | equid 2015 |
. . . . . . . 8
⊢ 𝑥 = 𝑥 |
3 | 2 | a1i 11 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → 𝑥 = 𝑥) |
4 | 3 | ax-gen 1798 |
. . . . . 6
⊢
∀𝑥(𝑥 = 𝑦 → 𝑥 = 𝑥) |
5 | 4 | a1i 11 |
. . . . 5
⊢ (𝑥 = 𝑥 → ∀𝑥(𝑥 = 𝑦 → 𝑥 = 𝑥)) |
6 | | equequ1 2028 |
. . . . . . . . 9
⊢ (𝑥 = 𝑧 → (𝑥 = 𝑥 ↔ 𝑧 = 𝑥)) |
7 | | equequ2 2029 |
. . . . . . . . 9
⊢ (𝑥 = 𝑤 → (𝑧 = 𝑥 ↔ 𝑧 = 𝑤)) |
8 | 6, 7 | sylan9bb 510 |
. . . . . . . 8
⊢ ((𝑥 = 𝑧 ∧ 𝑥 = 𝑤) → (𝑥 = 𝑥 ↔ 𝑧 = 𝑤)) |
9 | 8 | sps-o 36922 |
. . . . . . 7
⊢
(∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤) → (𝑥 = 𝑥 ↔ 𝑧 = 𝑤)) |
10 | | nfa1-o 36929 |
. . . . . . . 8
⊢
Ⅎ𝑥∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤) |
11 | 9 | imbi2d 341 |
. . . . . . . 8
⊢
(∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤) → ((𝑥 = 𝑦 → 𝑥 = 𝑥) ↔ (𝑥 = 𝑦 → 𝑧 = 𝑤))) |
12 | 10, 11 | albid 2215 |
. . . . . . 7
⊢
(∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤) → (∀𝑥(𝑥 = 𝑦 → 𝑥 = 𝑥) ↔ ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤))) |
13 | 9, 12 | imbi12d 345 |
. . . . . 6
⊢
(∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤) → ((𝑥 = 𝑥 → ∀𝑥(𝑥 = 𝑦 → 𝑥 = 𝑥)) ↔ (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤)))) |
14 | 13 | adantr 481 |
. . . . 5
⊢
((∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → ((𝑥 = 𝑥 → ∀𝑥(𝑥 = 𝑦 → 𝑥 = 𝑥)) ↔ (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤)))) |
15 | 5, 14 | mpbii 232 |
. . . 4
⊢
((∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤))) |
16 | 15 | exp32 421 |
. . 3
⊢
(∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤))))) |
17 | 1, 16 | sylbir 234 |
. 2
⊢
((∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤))))) |
18 | | equequ1 2028 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑥 = 𝑤 ↔ 𝑦 = 𝑤)) |
19 | 18 | ad2antll 726 |
. . . . . 6
⊢ ((¬
∀𝑥 𝑥 = 𝑤 ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑥 = 𝑤 ↔ 𝑦 = 𝑤)) |
20 | | axc9 2382 |
. . . . . . . . 9
⊢ (¬
∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑥 𝑥 = 𝑤 → (𝑦 = 𝑤 → ∀𝑥 𝑦 = 𝑤))) |
21 | 20 | impcom 408 |
. . . . . . . 8
⊢ ((¬
∀𝑥 𝑥 = 𝑤 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → (𝑦 = 𝑤 → ∀𝑥 𝑦 = 𝑤)) |
22 | 21 | adantrr 714 |
. . . . . . 7
⊢ ((¬
∀𝑥 𝑥 = 𝑤 ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑦 = 𝑤 → ∀𝑥 𝑦 = 𝑤)) |
23 | | equtrr 2025 |
. . . . . . . 8
⊢ (𝑦 = 𝑤 → (𝑥 = 𝑦 → 𝑥 = 𝑤)) |
24 | 23 | alimi 1814 |
. . . . . . 7
⊢
(∀𝑥 𝑦 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑥 = 𝑤)) |
25 | 22, 24 | syl6 35 |
. . . . . 6
⊢ ((¬
∀𝑥 𝑥 = 𝑤 ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑦 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑥 = 𝑤))) |
26 | 19, 25 | sylbid 239 |
. . . . 5
⊢ ((¬
∀𝑥 𝑥 = 𝑤 ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑥 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑥 = 𝑤))) |
27 | 26 | adantll 711 |
. . . 4
⊢
(((∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑥 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑥 = 𝑤))) |
28 | | equequ1 2028 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → (𝑥 = 𝑤 ↔ 𝑧 = 𝑤)) |
29 | 28 | sps-o 36922 |
. . . . . 6
⊢
(∀𝑥 𝑥 = 𝑧 → (𝑥 = 𝑤 ↔ 𝑧 = 𝑤)) |
30 | 29 | imbi2d 341 |
. . . . . . 7
⊢
(∀𝑥 𝑥 = 𝑧 → ((𝑥 = 𝑦 → 𝑥 = 𝑤) ↔ (𝑥 = 𝑦 → 𝑧 = 𝑤))) |
31 | 30 | dral2-o 36944 |
. . . . . 6
⊢
(∀𝑥 𝑥 = 𝑧 → (∀𝑥(𝑥 = 𝑦 → 𝑥 = 𝑤) ↔ ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤))) |
32 | 29, 31 | imbi12d 345 |
. . . . 5
⊢
(∀𝑥 𝑥 = 𝑧 → ((𝑥 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑥 = 𝑤)) ↔ (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤)))) |
33 | 32 | ad2antrr 723 |
. . . 4
⊢
(((∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → ((𝑥 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑥 = 𝑤)) ↔ (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤)))) |
34 | 27, 33 | mpbid 231 |
. . 3
⊢
(((∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤))) |
35 | 34 | exp32 421 |
. 2
⊢
((∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤))))) |
36 | | equequ2 2029 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 ↔ 𝑧 = 𝑦)) |
37 | 36 | ad2antll 726 |
. . . . . 6
⊢ ((¬
∀𝑥 𝑥 = 𝑧 ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑧 = 𝑥 ↔ 𝑧 = 𝑦)) |
38 | | axc9 2382 |
. . . . . . . . 9
⊢ (¬
∀𝑥 𝑥 = 𝑧 → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦))) |
39 | 38 | imp 407 |
. . . . . . . 8
⊢ ((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → (𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦)) |
40 | 39 | adantrr 714 |
. . . . . . 7
⊢ ((¬
∀𝑥 𝑥 = 𝑧 ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦)) |
41 | 36 | biimprcd 249 |
. . . . . . . 8
⊢ (𝑧 = 𝑦 → (𝑥 = 𝑦 → 𝑧 = 𝑥)) |
42 | 41 | alimi 1814 |
. . . . . . 7
⊢
(∀𝑥 𝑧 = 𝑦 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑥)) |
43 | 40, 42 | syl6 35 |
. . . . . 6
⊢ ((¬
∀𝑥 𝑥 = 𝑧 ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑧 = 𝑦 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑥))) |
44 | 37, 43 | sylbid 239 |
. . . . 5
⊢ ((¬
∀𝑥 𝑥 = 𝑧 ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑧 = 𝑥 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑥))) |
45 | 44 | adantlr 712 |
. . . 4
⊢ (((¬
∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑧 = 𝑥 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑥))) |
46 | 7 | sps-o 36922 |
. . . . . 6
⊢
(∀𝑥 𝑥 = 𝑤 → (𝑧 = 𝑥 ↔ 𝑧 = 𝑤)) |
47 | 46 | imbi2d 341 |
. . . . . . 7
⊢
(∀𝑥 𝑥 = 𝑤 → ((𝑥 = 𝑦 → 𝑧 = 𝑥) ↔ (𝑥 = 𝑦 → 𝑧 = 𝑤))) |
48 | 47 | dral2-o 36944 |
. . . . . 6
⊢
(∀𝑥 𝑥 = 𝑤 → (∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑥) ↔ ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤))) |
49 | 46, 48 | imbi12d 345 |
. . . . 5
⊢
(∀𝑥 𝑥 = 𝑤 → ((𝑧 = 𝑥 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑥)) ↔ (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤)))) |
50 | 49 | ad2antlr 724 |
. . . 4
⊢ (((¬
∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → ((𝑧 = 𝑥 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑥)) ↔ (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤)))) |
51 | 45, 50 | mpbid 231 |
. . 3
⊢ (((¬
∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤))) |
52 | 51 | exp32 421 |
. 2
⊢ ((¬
∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤))))) |
53 | | ax6ev 1973 |
. . . . 5
⊢
∃𝑢 𝑢 = 𝑤 |
54 | | ax6ev 1973 |
. . . . . . 7
⊢
∃𝑣 𝑣 = 𝑧 |
55 | | ax-1 6 |
. . . . . . . . . . 11
⊢ (𝑣 = 𝑢 → (𝑥 = 𝑦 → 𝑣 = 𝑢)) |
56 | 55 | alrimiv 1930 |
. . . . . . . . . 10
⊢ (𝑣 = 𝑢 → ∀𝑥(𝑥 = 𝑦 → 𝑣 = 𝑢)) |
57 | | equequ1 2028 |
. . . . . . . . . . . . 13
⊢ (𝑣 = 𝑧 → (𝑣 = 𝑢 ↔ 𝑧 = 𝑢)) |
58 | | equequ2 2029 |
. . . . . . . . . . . . 13
⊢ (𝑢 = 𝑤 → (𝑧 = 𝑢 ↔ 𝑧 = 𝑤)) |
59 | 57, 58 | sylan9bb 510 |
. . . . . . . . . . . 12
⊢ ((𝑣 = 𝑧 ∧ 𝑢 = 𝑤) → (𝑣 = 𝑢 ↔ 𝑧 = 𝑤)) |
60 | 59 | adantl 482 |
. . . . . . . . . . 11
⊢ (((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧 ∧ 𝑢 = 𝑤)) → (𝑣 = 𝑢 ↔ 𝑧 = 𝑤)) |
61 | | dveeq2-o 36947 |
. . . . . . . . . . . . . . 15
⊢ (¬
∀𝑥 𝑥 = 𝑧 → (𝑣 = 𝑧 → ∀𝑥 𝑣 = 𝑧)) |
62 | | dveeq2-o 36947 |
. . . . . . . . . . . . . . 15
⊢ (¬
∀𝑥 𝑥 = 𝑤 → (𝑢 = 𝑤 → ∀𝑥 𝑢 = 𝑤)) |
63 | 61, 62 | im2anan9 620 |
. . . . . . . . . . . . . 14
⊢ ((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → ((𝑣 = 𝑧 ∧ 𝑢 = 𝑤) → (∀𝑥 𝑣 = 𝑧 ∧ ∀𝑥 𝑢 = 𝑤))) |
64 | 63 | imp 407 |
. . . . . . . . . . . . 13
⊢ (((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧 ∧ 𝑢 = 𝑤)) → (∀𝑥 𝑣 = 𝑧 ∧ ∀𝑥 𝑢 = 𝑤)) |
65 | | 19.26 1873 |
. . . . . . . . . . . . 13
⊢
(∀𝑥(𝑣 = 𝑧 ∧ 𝑢 = 𝑤) ↔ (∀𝑥 𝑣 = 𝑧 ∧ ∀𝑥 𝑢 = 𝑤)) |
66 | 64, 65 | sylibr 233 |
. . . . . . . . . . . 12
⊢ (((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧 ∧ 𝑢 = 𝑤)) → ∀𝑥(𝑣 = 𝑧 ∧ 𝑢 = 𝑤)) |
67 | | nfa1-o 36929 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥∀𝑥(𝑣 = 𝑧 ∧ 𝑢 = 𝑤) |
68 | 59 | sps-o 36922 |
. . . . . . . . . . . . . 14
⊢
(∀𝑥(𝑣 = 𝑧 ∧ 𝑢 = 𝑤) → (𝑣 = 𝑢 ↔ 𝑧 = 𝑤)) |
69 | 68 | imbi2d 341 |
. . . . . . . . . . . . 13
⊢
(∀𝑥(𝑣 = 𝑧 ∧ 𝑢 = 𝑤) → ((𝑥 = 𝑦 → 𝑣 = 𝑢) ↔ (𝑥 = 𝑦 → 𝑧 = 𝑤))) |
70 | 67, 69 | albid 2215 |
. . . . . . . . . . . 12
⊢
(∀𝑥(𝑣 = 𝑧 ∧ 𝑢 = 𝑤) → (∀𝑥(𝑥 = 𝑦 → 𝑣 = 𝑢) ↔ ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤))) |
71 | 66, 70 | syl 17 |
. . . . . . . . . . 11
⊢ (((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧 ∧ 𝑢 = 𝑤)) → (∀𝑥(𝑥 = 𝑦 → 𝑣 = 𝑢) ↔ ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤))) |
72 | 60, 71 | imbi12d 345 |
. . . . . . . . . 10
⊢ (((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧 ∧ 𝑢 = 𝑤)) → ((𝑣 = 𝑢 → ∀𝑥(𝑥 = 𝑦 → 𝑣 = 𝑢)) ↔ (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤)))) |
73 | 56, 72 | mpbii 232 |
. . . . . . . . 9
⊢ (((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧 ∧ 𝑢 = 𝑤)) → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤))) |
74 | 73 | exp32 421 |
. . . . . . . 8
⊢ ((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (𝑣 = 𝑧 → (𝑢 = 𝑤 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤))))) |
75 | 74 | exlimdv 1936 |
. . . . . . 7
⊢ ((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (∃𝑣 𝑣 = 𝑧 → (𝑢 = 𝑤 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤))))) |
76 | 54, 75 | mpi 20 |
. . . . . 6
⊢ ((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (𝑢 = 𝑤 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤)))) |
77 | 76 | exlimdv 1936 |
. . . . 5
⊢ ((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (∃𝑢 𝑢 = 𝑤 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤)))) |
78 | 53, 77 | mpi 20 |
. . . 4
⊢ ((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤))) |
79 | 78 | a1d 25 |
. . 3
⊢ ((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (𝑥 = 𝑦 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤)))) |
80 | 79 | a1d 25 |
. 2
⊢ ((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤))))) |
81 | 17, 35, 52, 80 | 4cases 1038 |
1
⊢ (¬
∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 = 𝑤)))) |