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

Definition df-s6 13396
Description: Define the length 6 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.)
Assertion
Ref Expression
df-s6 ⟨“𝐴𝐵𝐶𝐷𝐸𝐹”⟩ = (⟨“𝐴𝐵𝐶𝐷𝐸”⟩ ++ ⟨“𝐹”⟩)

Detailed syntax breakdown of Definition df-s6
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 𝐹
71, 2, 3, 4, 5, 6cs6 13389 . 2 class ⟨“𝐴𝐵𝐶𝐷𝐸𝐹”⟩
81, 2, 3, 4, 5cs5 13388 . . 3 class ⟨“𝐴𝐵𝐶𝐷𝐸”⟩
96cs1 13097 . . 3 class ⟨“𝐹”⟩
10 cconcat 13096 . . 3 class ++
118, 9, 10co 6526 . 2 class (⟨“𝐴𝐵𝐶𝐷𝐸”⟩ ++ ⟨“𝐹”⟩)
127, 11wceq 1474 1 wff ⟨“𝐴𝐵𝐶𝐷𝐸𝐹”⟩ = (⟨“𝐴𝐵𝐶𝐷𝐸”⟩ ++ ⟨“𝐹”⟩)
Colors of variables: wff setvar class
This definition is referenced by:  s6eqd  13411  s6cld  13418  s6cli  13427  s6len  13444  s1s5  13469  s1s6  13470  s4s2  13473  konigsberg  26307  konigsberglem1  41403  konigsberglem2  41404  konigsberglem3  41405
  Copyright terms: Public domain W3C validator