![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-s2 | Structured version Visualization version GIF version |
Description: Define the length 2 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.) |
Ref | Expression |
---|---|
df-s2 | ⊢ 〈“𝐴𝐵”〉 = (〈“𝐴”〉 ++ 〈“𝐵”〉) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class 𝐴 | |
2 | cB | . . 3 class 𝐵 | |
3 | 1, 2 | cs2 14779 | . 2 class 〈“𝐴𝐵”〉 |
4 | 1 | cs1 14532 | . . 3 class 〈“𝐴”〉 |
5 | 2 | cs1 14532 | . . 3 class 〈“𝐵”〉 |
6 | cconcat 14507 | . . 3 class ++ | |
7 | 4, 5, 6 | co 7396 | . 2 class (〈“𝐴”〉 ++ 〈“𝐵”〉) |
8 | 3, 7 | wceq 1542 | 1 wff 〈“𝐴𝐵”〉 = (〈“𝐴”〉 ++ 〈“𝐵”〉) |
Colors of variables: wff setvar class |
This definition is referenced by: cats2cat 14800 s2eqd 14801 s2cld 14809 s2cli 14818 s2fv0 14825 s2fv1 14826 s2len 14827 s2prop 14845 s2co 14858 s1s2 14861 s2s2 14867 s4s2 14868 s2s5 14872 s5s2 14873 s2eq2s1eq 14874 swrds2 14878 repsw2 14888 ccatw2s1ccatws2 14892 ofs2 14905 gsumws2 18710 efginvrel2 19579 efgredlemc 19597 frgpnabllem1 19724 2pthon3v 29164 konigsberglem1 29472 konigsberglem2 29473 konigsberglem3 29474 cshw1s2 32095 ofcs2 33487 |
Copyright terms: Public domain | W3C validator |