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 14200
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 14193 . 2 class ⟨“𝐴𝐵𝐶𝐷”⟩
61, 2, 3cs3 14192 . . 3 class ⟨“𝐴𝐵𝐶”⟩
74cs1 13937 . . 3 class ⟨“𝐷”⟩
8 cconcat 13910 . . 3 class ++
96, 7, 8co 7145 . 2 class (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)
105, 9wceq 1528 1 wff ⟨“𝐴𝐵𝐶𝐷”⟩ = (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)
Colors of variables: wff setvar class
This definition is referenced by:  s4eqd  14215  s4cld  14223  s4cli  14232  s4fv0  14245  s4fv1  14246  s4fv2  14247  s4fv3  14248  s4len  14249  s4prop  14260  s1s3  14274  s1s4  14275  s2s2  14279  s4s4  14282  tgcgr4  26244  konigsberglem1  27958  konigsberglem2  27959  konigsberglem3  27960
  Copyright terms: Public domain W3C validator