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

Definition df-s3 12981
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 12974 . 2  class  <" A B C ">
51, 2cs2 12973 . . 3  class  <" A B ">
63cs1 12691 . . 3  class  <" C ">
7 cconcat 12690 . . 3  class ++
85, 6, 7co 6314 . 2  class  ( <" A B "> ++  <" C "> )
94, 8wceq 1454 1  wff  <" A B C ">  =  ( <" A B "> ++  <" C "> )
Colors of variables: wff setvar class
This definition is referenced by:  s3eqd  12995  s3cld  13002  s3cli  13011  s3fv0  13021  s3fv1  13022  s3fv2  13023  s3len  13024  s3tpop  13039  s4prop  13040  s3co  13051  s1s2  13053  s1s3  13054  s2s2  13059  s4s3  13061  repsw3  13074  konigsberg  25763  2pthon3v-av  39891
  Copyright terms: Public domain W3C validator