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

Definition df-s3 12725
Description: Define the length 3 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.)
Assertion
Ref Expression
df-s3  |-  <" A B C ">  =  ( <" A B "> ++  <" 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 12718 . 2  class  <" A B C ">
51, 2cs2 12717 . . 3  class  <" A B ">
63cs1 12441 . . 3  class  <" C ">
7 cconcat 12440 . . 3  class ++
85, 6, 7co 6196 . 2  class  ( <" A B "> ++  <" C "> )
94, 8wceq 1399 1  wff  <" A B C ">  =  ( <" A B "> ++  <" C "> )
Colors of variables: wff setvar class
This definition is referenced by:  s3eqd  12739  s3cld  12746  s3cli  12755  s3fv0  12764  s3fv1  12765  s3fv2  12766  s3len  12767  s4prop  12774  s3co  12780  s1s2  12782  s1s3  12783  s2s2  12788  s4s3  12790  repsw3  12800  konigsberg  25108
  Copyright terms: Public domain W3C validator