Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-s3 | Structured version Visualization version GIF version |
Description: Define the length 3 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.) |
Ref | Expression |
---|---|
df-s3 | ⊢ 〈“𝐴𝐵𝐶”〉 = (〈“𝐴𝐵”〉 ++ 〈“𝐶”〉) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class 𝐴 | |
2 | cB | . . 3 class 𝐵 | |
3 | cC | . . 3 class 𝐶 | |
4 | 1, 2, 3 | cs3 14194 | . 2 class 〈“𝐴𝐵𝐶”〉 |
5 | 1, 2 | cs2 14193 | . . 3 class 〈“𝐴𝐵”〉 |
6 | 3 | cs1 13939 | . . 3 class 〈“𝐶”〉 |
7 | cconcat 13912 | . . 3 class ++ | |
8 | 5, 6, 7 | co 7145 | . 2 class (〈“𝐴𝐵”〉 ++ 〈“𝐶”〉) |
9 | 4, 8 | wceq 1528 | 1 wff 〈“𝐴𝐵𝐶”〉 = (〈“𝐴𝐵”〉 ++ 〈“𝐶”〉) |
Colors of variables: wff setvar class |
This definition is referenced by: s3eqd 14216 s3cld 14224 s3cli 14233 s3fv0 14243 s3fv1 14244 s3fv2 14245 s3len 14246 s3tpop 14261 s4prop 14262 s3co 14273 s1s2 14275 s1s3 14276 s2s2 14281 s4s3 14283 s3s4 14285 s3eqs2s1eq 14290 repsw3 14303 2pthon3v 27650 konigsberglem1 27959 konigsberglem2 27960 konigsberglem3 27961 |
Copyright terms: Public domain | W3C validator |