![]() |
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 14790 | . 2 class 〈“𝐴𝐵𝐶𝐷”〉 |
6 | 1, 2, 3 | cs3 14789 | . . 3 class 〈“𝐴𝐵𝐶”〉 |
7 | 4 | cs1 14541 | . . 3 class 〈“𝐷”〉 |
8 | cconcat 14516 | . . 3 class ++ | |
9 | 6, 7, 8 | co 7401 | . 2 class (〈“𝐴𝐵𝐶”〉 ++ 〈“𝐷”〉) |
10 | 5, 9 | wceq 1533 | 1 wff 〈“𝐴𝐵𝐶𝐷”〉 = (〈“𝐴𝐵𝐶”〉 ++ 〈“𝐷”〉) |
Colors of variables: wff setvar class |
This definition is referenced by: s4eqd 14812 s4cld 14820 s4cli 14829 s4fv0 14842 s4fv1 14843 s4fv2 14844 s4fv3 14845 s4len 14846 s4prop 14857 s1s3 14871 s1s4 14872 s2s2 14876 s4s4 14879 tgcgr4 28206 konigsberglem1 29929 konigsberglem2 29930 konigsberglem3 29931 |
Copyright terms: Public domain | W3C validator |