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 13815
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 13808 . 2 class ⟨“𝐴𝐵𝐶𝐷”⟩
61, 2, 3cs3 13807 . . 3 class ⟨“𝐴𝐵𝐶”⟩
74cs1 13500 . . 3 class ⟨“𝐷”⟩
8 cconcat 13499 . . 3 class ++
96, 7, 8co 6814 . 2 class (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)
105, 9wceq 1632 1 wff ⟨“𝐴𝐵𝐶𝐷”⟩ = (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)
Colors of variables: wff setvar class
This definition is referenced by:  s4eqd  13830  s4cld  13838  s4cli  13847  s4fv0  13860  s4fv1  13861  s4fv2  13862  s4fv3  13863  s4len  13864  s4prop  13875  s1s3  13889  s1s4  13890  s2s2  13894  s4s4  13897  tgcgr4  25646  konigsberglem1  27425  konigsberglem2  27426  konigsberglem3  27427
  Copyright terms: Public domain W3C validator