| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > df-s6 | Structured version Visualization version GIF version | ||
| Description: Define the length 6 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.) |
| Ref | Expression |
|---|---|
| df-s6 | ⊢ 〈“𝐴𝐵𝐶𝐷𝐸𝐹”〉 = (〈“𝐴𝐵𝐶𝐷𝐸”〉 ++ 〈“𝐹”〉) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cA | . . 3 class 𝐴 | |
| 2 | cB | . . 3 class 𝐵 | |
| 3 | cC | . . 3 class 𝐶 | |
| 4 | cD | . . 3 class 𝐷 | |
| 5 | cE | . . 3 class 𝐸 | |
| 6 | cF | . . 3 class 𝐹 | |
| 7 | 1, 2, 3, 4, 5, 6 | cs6 14884 | . 2 class 〈“𝐴𝐵𝐶𝐷𝐸𝐹”〉 |
| 8 | 1, 2, 3, 4, 5 | cs5 14883 | . . 3 class 〈“𝐴𝐵𝐶𝐷𝐸”〉 |
| 9 | 6 | cs1 14633 | . . 3 class 〈“𝐹”〉 |
| 10 | cconcat 14608 | . . 3 class ++ | |
| 11 | 8, 9, 10 | co 7431 | . 2 class (〈“𝐴𝐵𝐶𝐷𝐸”〉 ++ 〈“𝐹”〉) |
| 12 | 7, 11 | wceq 1540 | 1 wff 〈“𝐴𝐵𝐶𝐷𝐸𝐹”〉 = (〈“𝐴𝐵𝐶𝐷𝐸”〉 ++ 〈“𝐹”〉) |
| Colors of variables: wff setvar class |
| This definition is referenced by: s6eqd 14906 s6cld 14914 s6cli 14923 s6len 14940 s1s5 14965 s1s6 14966 s4s2 14969 konigsberglem1 30271 konigsberglem2 30272 konigsberglem3 30273 |
| Copyright terms: Public domain | W3C validator |