![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-s4 | Structured version Visualization version GIF version |
Description: Define the length 4 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.) |
Ref | Expression |
---|---|
df-s4 | ⊢ 〈“𝐴𝐵𝐶𝐷”〉 = (〈“𝐴𝐵𝐶”〉 ++ 〈“𝐷”〉) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class 𝐴 | |
2 | cB | . . 3 class 𝐵 | |
3 | cC | . . 3 class 𝐶 | |
4 | cD | . . 3 class 𝐷 | |
5 | 1, 2, 3, 4 | cs4 14057 | . 2 class 〈“𝐴𝐵𝐶𝐷”〉 |
6 | 1, 2, 3 | cs3 14056 | . . 3 class 〈“𝐴𝐵𝐶”〉 |
7 | 4 | cs1 13748 | . . 3 class 〈“𝐷”〉 |
8 | cconcat 13723 | . . 3 class ++ | |
9 | 6, 7, 8 | co 6970 | . 2 class (〈“𝐴𝐵𝐶”〉 ++ 〈“𝐷”〉) |
10 | 5, 9 | wceq 1507 | 1 wff 〈“𝐴𝐵𝐶𝐷”〉 = (〈“𝐴𝐵𝐶”〉 ++ 〈“𝐷”〉) |
Colors of variables: wff setvar class |
This definition is referenced by: s4eqd 14079 s4cld 14087 s4cli 14096 s4fv0 14109 s4fv1 14110 s4fv2 14111 s4fv3 14112 s4len 14113 s4prop 14124 s1s3 14138 s1s4 14139 s2s2 14143 s4s4 14146 tgcgr4 26009 konigsberglem1 27774 konigsberglem2 27775 konigsberglem3 27776 |
Copyright terms: Public domain | W3C validator |