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

Definition df-s8 13396
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 class 𝐴
2 cB . . 3 class 𝐵
3 cC . . 3 class 𝐶
4 cD . . 3 class 𝐷
5 cE . . 3 class 𝐸
6 cF . . 3 class 𝐹
7 cG . . 3 class 𝐺
8 cH . . 3 class 𝐻
91, 2, 3, 4, 5, 6, 7, 8cs8 13389 . 2 class ⟨“𝐴𝐵𝐶𝐷𝐸𝐹𝐺𝐻”⟩
101, 2, 3, 4, 5, 6, 7cs7 13388 . . 3 class ⟨“𝐴𝐵𝐶𝐷𝐸𝐹𝐺”⟩
118cs1 13095 . . 3 class ⟨“𝐻”⟩
12 cconcat 13094 . . 3 class ++
1310, 11, 12co 6527 . 2 class (⟨“𝐴𝐵𝐶𝐷𝐸𝐹𝐺”⟩ ++ ⟨“𝐻”⟩)
149, 13wceq 1474 1 wff ⟨“𝐴𝐵𝐶𝐷𝐸𝐹𝐺𝐻”⟩ = (⟨“𝐴𝐵𝐶𝐷𝐸𝐹𝐺”⟩ ++ ⟨“𝐻”⟩)
Colors of variables: wff setvar class
This definition is referenced by:  s8eqd  13411  s8cld  13418  s8cli  13427  s8len  13444  s1s7  13469  s4s4  13473
  Copyright terms: Public domain W3C validator