![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-s2 | Structured version Visualization version Unicode 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
![]() ![]() | |
2 | cB |
. . 3
![]() ![]() | |
3 | 1, 2 | cs2 12980 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1 | cs1 12698 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() |
5 | 2 | cs1 12698 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() |
6 | cconcat 12697 |
. . 3
![]() | |
7 | 4, 5, 6 | co 6320 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | 3, 7 | wceq 1455 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
This definition is referenced by: s2eqd 13001 s2cld 13008 s2cli 13017 s2fv0 13024 s2fv1 13025 s2len 13026 s2prop 13044 s2co 13057 s1s2 13060 s2s2 13066 s4s2 13067 s2eq2s1eq 13070 swrds2 13072 repsw2 13080 ccatw2s1ccatws2 13084 gsumws2 16681 efginvrel2 17432 efgredlemc 17450 frgpnabllem1 17564 konigsberg 25771 ofs2 29483 ofcs2 29484 2pthon3v-av 39988 |
Copyright terms: Public domain | W3C validator |