![]() |
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 13633 | . 2 class 〈“𝐴𝐵𝐶”〉 |
5 | 1, 2 | cs2 13632 | . . 3 class 〈“𝐴𝐵”〉 |
6 | 3 | cs1 13326 | . . 3 class 〈“𝐶”〉 |
7 | cconcat 13325 | . . 3 class ++ | |
8 | 5, 6, 7 | co 6690 | . 2 class (〈“𝐴𝐵”〉 ++ 〈“𝐶”〉) |
9 | 4, 8 | wceq 1523 | 1 wff 〈“𝐴𝐵𝐶”〉 = (〈“𝐴𝐵”〉 ++ 〈“𝐶”〉) |
Colors of variables: wff setvar class |
This definition is referenced by: s3eqd 13655 s3cld 13663 s3cli 13672 s3fv0 13682 s3fv1 13683 s3fv2 13684 s3len 13685 s3tpop 13700 s4prop 13701 s3co 13712 s1s2 13714 s1s3 13715 s2s2 13720 s4s3 13722 s3s4 13724 s3eqs2s1eq 13729 repsw3 13740 2pthon3v 26908 konigsberglem1 27230 konigsberglem2 27231 konigsberglem3 27232 |
Copyright terms: Public domain | W3C validator |