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

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

Detailed syntax breakdown of Definition df-s7
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 𝐺
81, 2, 3, 4, 5, 6, 7cs7 14196 . 2 class ⟨“𝐴𝐵𝐶𝐷𝐸𝐹𝐺”⟩
91, 2, 3, 4, 5, 6cs6 14195 . . 3 class ⟨“𝐴𝐵𝐶𝐷𝐸𝐹”⟩
107cs1 13937 . . 3 class ⟨“𝐺”⟩
11 cconcat 13910 . . 3 class ++
129, 10, 11co 7145 . 2 class (⟨“𝐴𝐵𝐶𝐷𝐸𝐹”⟩ ++ ⟨“𝐺”⟩)
138, 12wceq 1528 1 wff ⟨“𝐴𝐵𝐶𝐷𝐸𝐹𝐺”⟩ = (⟨“𝐴𝐵𝐶𝐷𝐸𝐹”⟩ ++ ⟨“𝐺”⟩)
Colors of variables: wff setvar class
This definition is referenced by:  s7eqd  14218  s7cld  14226  s7cli  14235  s7len  14252  s1s6  14277  s1s7  14278  s4s3  14281  s5s2  14285  konigsberglem1  27958  konigsberglem2  27959  konigsberglem3  27960
  Copyright terms: Public domain W3C validator