MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-s4 Structured version   Unicode version

Definition df-s4 12772
Description: Define the length 4 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.)
Assertion
Ref Expression
df-s4  |-  <" A B C D ">  =  ( <" A B C "> concat  <" D "> )

Detailed syntax breakdown of Definition df-s4
StepHypRef Expression
1 cA . . 3  class  A
2 cB . . 3  class  B
3 cC . . 3  class  C
4 cD . . 3  class  D
51, 2, 3, 4cs4 12765 . 2  class  <" A B C D ">
61, 2, 3cs3 12764 . . 3  class  <" A B C ">
74cs1 12497 . . 3  class  <" D ">
8 cconcat 12496 . . 3  class concat
96, 7, 8co 6282 . 2  class  ( <" A B C "> concat  <" D "> )
105, 9wceq 1379 1  wff  <" A B C D ">  =  ( <" A B C "> concat  <" D "> )
Colors of variables: wff setvar class
This definition is referenced by:  s4eqd  12786  s4cld  12793  s4cli  12802  s4len  12814  s4prop  12820  s1s3  12829  s1s4  12830  s2s2  12834  s4s4  12837  usgraexmplvtx  24075  konigsberg  24660
  Copyright terms: Public domain W3C validator