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 14191 | . 2 class 〈“𝐴𝐵”〉 |
4 | 1 | cs1 13937 | . . 3 class 〈“𝐴”〉 |
5 | 2 | cs1 13937 | . . 3 class 〈“𝐵”〉 |
6 | cconcat 13910 | . . 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 14212 s2eqd 14213 s2cld 14221 s2cli 14230 s2fv0 14237 s2fv1 14238 s2len 14239 s2prop 14257 s2co 14270 s1s2 14273 s2s2 14279 s4s2 14280 s2s5 14284 s5s2 14285 s2eq2s1eq 14286 swrds2 14290 repsw2 14300 ccatw2s1ccatws2 14304 ccatw2s1ccatws2OLD 14305 ofs2 14319 gsumws2 17995 efginvrel2 18782 efgredlemc 18800 frgpnabllem1 18922 2pthon3v 27649 konigsberglem1 27958 konigsberglem2 27959 konigsberglem3 27960 cshw1s2 30561 ofcs2 31714 |
Copyright terms: Public domain | W3C validator |