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

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

Detailed syntax breakdown of Definition df-s5
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cB . . 3 class 𝐵
3 cC . . 3 class 𝐶
4 cD . . 3 class 𝐷
5 cE . . 3 class 𝐸
61, 2, 3, 4, 5cs5 13386 . 2 class ⟨“𝐴𝐵𝐶𝐷𝐸”⟩
71, 2, 3, 4cs4 13385 . . 3 class ⟨“𝐴𝐵𝐶𝐷”⟩
85cs1 13095 . . 3 class ⟨“𝐸”⟩
9 cconcat 13094 . . 3 class ++
107, 8, 9co 6527 . 2 class (⟨“𝐴𝐵𝐶𝐷”⟩ ++ ⟨“𝐸”⟩)
116, 10wceq 1474 1 wff ⟨“𝐴𝐵𝐶𝐷𝐸”⟩ = (⟨“𝐴𝐵𝐶𝐷”⟩ ++ ⟨“𝐸”⟩)
Colors of variables: wff setvar class
This definition is referenced by:  s5eqd  13408  s5cld  13415  s5cli  13424  s5len  13441  s1s4  13466  s1s5  13467  s4s2  13471  s5s2  13476  konigsberg  26280  konigsberglem1  41417  konigsberglem2  41418  konigsberglem3  41419
  Copyright terms: Public domain W3C validator