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 14193 | . 2 class 〈“𝐴𝐵𝐶𝐷”〉 |
6 | 1, 2, 3 | cs3 14192 | . . 3 class 〈“𝐴𝐵𝐶”〉 |
7 | 4 | cs1 13937 | . . 3 class 〈“𝐷”〉 |
8 | cconcat 13910 | . . 3 class ++ | |
9 | 6, 7, 8 | co 7145 | . 2 class (〈“𝐴𝐵𝐶”〉 ++ 〈“𝐷”〉) |
10 | 5, 9 | wceq 1528 | 1 wff 〈“𝐴𝐵𝐶𝐷”〉 = (〈“𝐴𝐵𝐶”〉 ++ 〈“𝐷”〉) |
Colors of variables: wff setvar class |
This definition is referenced by: s4eqd 14215 s4cld 14223 s4cli 14232 s4fv0 14245 s4fv1 14246 s4fv2 14247 s4fv3 14248 s4len 14249 s4prop 14260 s1s3 14274 s1s4 14275 s2s2 14279 s4s4 14282 tgcgr4 26244 konigsberglem1 27958 konigsberglem2 27959 konigsberglem3 27960 |
Copyright terms: Public domain | W3C validator |