MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-s8 Unicode version

Definition df-s8 12639
Description: Define the length 8 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.)
Assertion
Ref Expression
df-s8

Detailed syntax breakdown of Definition df-s8
StepHypRef Expression
1 cA . . 3
2 cB . . 3
3 cC . . 3
4 cD . . 3
5 cE . . 3
6 cF . . 3
7 cG . . 3
8 cH . . 3
91, 2, 3, 4, 5, 6, 7, 8cs8 12632 . 2
101, 2, 3, 4, 5, 6, 7cs7 12631 . . 3
118cs1 12382 . . 3
12 cconcat 12381 . . 3
1310, 11, 12co 6222 . 2
149, 13wceq 1370 1
Colors of variables: wff setvar class
This definition is referenced by:  s8eqd  12653  s8cld  12660  s8cli  12669  s8len  12681  s1s7  12696  s4s4  12700
  Copyright terms: Public domain W3C validator