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

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

Detailed syntax breakdown of Definition df-s4
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cB . . 3 class 𝐵
3 cC . . 3 class 𝐶
4 cD . . 3 class 𝐷
51, 2, 3, 4cs4 14057 . 2 class ⟨“𝐴𝐵𝐶𝐷”⟩
61, 2, 3cs3 14056 . . 3 class ⟨“𝐴𝐵𝐶”⟩
74cs1 13748 . . 3 class ⟨“𝐷”⟩
8 cconcat 13723 . . 3 class ++
96, 7, 8co 6970 . 2 class (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)
105, 9wceq 1507 1 wff ⟨“𝐴𝐵𝐶𝐷”⟩ = (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)
Colors of variables: wff setvar class
This definition is referenced by:  s4eqd  14079  s4cld  14087  s4cli  14096  s4fv0  14109  s4fv1  14110  s4fv2  14111  s4fv3  14112  s4len  14113  s4prop  14124  s1s3  14138  s1s4  14139  s2s2  14143  s4s4  14146  tgcgr4  26009  konigsberglem1  27774  konigsberglem2  27775  konigsberglem3  27776
  Copyright terms: Public domain W3C validator