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

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

Detailed syntax breakdown of Definition df-s3
StepHypRef Expression
1 cA . . 3  class  A
2 cB . . 3  class  B
3 cC . . 3  class  C
41, 2, 3cs3 12757 . 2  class  <" A B C ">
51, 2cs2 12756 . . 3  class  <" A B ">
63cs1 12490 . . 3  class  <" C ">
7 cconcat 12489 . . 3  class concat
85, 6, 7co 6275 . 2  class  ( <" A B "> concat 
<" C "> )
94, 8wceq 1374 1  wff  <" A B C ">  =  ( <" A B "> concat  <" C "> )
Colors of variables: wff setvar class
This definition is referenced by:  s3eqd  12778  s3cld  12785  s3cli  12794  s3fv0  12803  s3fv1  12804  s3fv2  12805  s3len  12806  s4prop  12813  s3co  12819  s1s2  12821  s1s3  12822  s2s2  12827  s4s3  12829  repsw3  12839  konigsberg  24649
  Copyright terms: Public domain W3C validator