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 14193 | . 2 class 〈“𝐴𝐵”〉 |
4 | 1 | cs1 13939 | . . 3 class 〈“𝐴”〉 |
5 | 2 | cs1 13939 | . . 3 class 〈“𝐵”〉 |
6 | cconcat 13912 | . . 3 class ++ | |
7 | 4, 5, 6 | co 7145 | . 2 class (〈“𝐴”〉 ++ 〈“𝐵”〉) |
8 | 3, 7 | wceq 1528 | 1 wff 〈“𝐴𝐵”〉 = (〈“𝐴”〉 ++ 〈“𝐵”〉) |
Colors of variables: wff setvar class |
This definition is referenced by: cats2cat 14214 s2eqd 14215 s2cld 14223 s2cli 14232 s2fv0 14239 s2fv1 14240 s2len 14241 s2prop 14259 s2co 14272 s1s2 14275 s2s2 14281 s4s2 14282 s2s5 14286 s5s2 14287 s2eq2s1eq 14288 swrds2 14292 repsw2 14302 ccatw2s1ccatws2 14306 ccatw2s1ccatws2OLD 14307 ofs2 14321 gsumws2 17997 efginvrel2 18784 efgredlemc 18802 frgpnabllem1 18924 2pthon3v 27650 konigsberglem1 27959 konigsberglem2 27960 konigsberglem3 27961 cshw1s2 30562 ofcs2 31715 |
Copyright terms: Public domain | W3C validator |