![]() |
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 13808 | . 2 class 〈“𝐴𝐵𝐶𝐷”〉 |
6 | 1, 2, 3 | cs3 13807 | . . 3 class 〈“𝐴𝐵𝐶”〉 |
7 | 4 | cs1 13500 | . . 3 class 〈“𝐷”〉 |
8 | cconcat 13499 | . . 3 class ++ | |
9 | 6, 7, 8 | co 6814 | . 2 class (〈“𝐴𝐵𝐶”〉 ++ 〈“𝐷”〉) |
10 | 5, 9 | wceq 1632 | 1 wff 〈“𝐴𝐵𝐶𝐷”〉 = (〈“𝐴𝐵𝐶”〉 ++ 〈“𝐷”〉) |
Colors of variables: wff setvar class |
This definition is referenced by: s4eqd 13830 s4cld 13838 s4cli 13847 s4fv0 13860 s4fv1 13861 s4fv2 13862 s4fv3 13863 s4len 13864 s4prop 13875 s1s3 13889 s1s4 13890 s2s2 13894 s4s4 13897 tgcgr4 25646 konigsberglem1 27425 konigsberglem2 27426 konigsberglem3 27427 |
Copyright terms: Public domain | W3C validator |