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 14215
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 14208 . 2 class ⟨“𝐴𝐵𝐶𝐷”⟩
61, 2, 3cs3 14207 . . 3 class ⟨“𝐴𝐵𝐶”⟩
74cs1 13952 . . 3 class ⟨“𝐷”⟩
8 cconcat 13925 . . 3 class ++
96, 7, 8co 7150 . 2 class (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)
105, 9wceq 1538 1 wff ⟨“𝐴𝐵𝐶𝐷”⟩ = (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)
Colors of variables: wff setvar class
This definition is referenced by:  s4eqd  14230  s4cld  14238  s4cli  14247  s4fv0  14260  s4fv1  14261  s4fv2  14262  s4fv3  14263  s4len  14264  s4prop  14275  s1s3  14289  s1s4  14290  s2s2  14294  s4s4  14297  tgcgr4  26331  konigsberglem1  28043  konigsberglem2  28044  konigsberglem3  28045
  Copyright terms: Public domain W3C validator