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 13795
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 13788 . 2 class ⟨“𝐴𝐵𝐶𝐷”⟩
61, 2, 3cs3 13787 . . 3 class ⟨“𝐴𝐵𝐶”⟩
74cs1 13480 . . 3 class ⟨“𝐷”⟩
8 cconcat 13479 . . 3 class ++
96, 7, 8co 6813 . 2 class (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)
105, 9wceq 1632 1 wff ⟨“𝐴𝐵𝐶𝐷”⟩ = (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)
Colors of variables: wff setvar class
This definition is referenced by:  s4eqd  13810  s4cld  13818  s4cli  13827  s4fv0  13840  s4fv1  13841  s4fv2  13842  s4fv3  13843  s4len  13844  s4prop  13855  s1s3  13869  s1s4  13870  s2s2  13874  s4s4  13877  tgcgr4  25625  konigsberglem1  27404  konigsberglem2  27405  konigsberglem3  27406
  Copyright terms: Public domain W3C validator