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 14889
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 14882 . 2 class ⟨“𝐴𝐵𝐶𝐷”⟩
61, 2, 3cs3 14881 . . 3 class ⟨“𝐴𝐵𝐶”⟩
74cs1 14633 . . 3 class ⟨“𝐷”⟩
8 cconcat 14608 . . 3 class ++
96, 7, 8co 7431 . 2 class (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)
105, 9wceq 1540 1 wff ⟨“𝐴𝐵𝐶𝐷”⟩ = (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)
Colors of variables: wff setvar class
This definition is referenced by:  s4eqd  14904  s4cld  14912  s4cli  14921  s4fv0  14934  s4fv1  14935  s4fv2  14936  s4fv3  14937  s4len  14938  s4prop  14949  s1s3  14963  s1s4  14964  s2s2  14968  s4s4  14971  s7rn  15004  tgcgr4  28539  konigsberglem1  30271  konigsberglem2  30272  konigsberglem3  30273
  Copyright terms: Public domain W3C validator