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

Definition df-s4 12937
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 "> ++  <" 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 12930 . 2  class  <" A B C D ">
61, 2, 3cs3 12929 . . 3  class  <" A B C ">
74cs1 12652 . . 3  class  <" D ">
8 cconcat 12651 . . 3  class ++
96, 7, 8co 6302 . 2  class  ( <" A B C "> ++  <" D "> )
105, 9wceq 1437 1  wff  <" A B C D ">  =  ( <" A B C "> ++  <" D "> )
Colors of variables: wff setvar class
This definition is referenced by:  s4eqd  12951  s4cld  12958  s4cli  12967  s4fv0  12979  s4fv1  12980  s4fv2  12981  s4fv3  12982  s4len  12983  s4prop  12989  s1s3  12998  s1s4  12999  s2s2  13003  s4s4  13006  tgcgr4  24563  usgraexmplvtx  25116  konigsberg  25701
  Copyright terms: Public domain W3C validator