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

Definition df-s3 12945
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 12938 . 2  class  <" A B C ">
51, 2cs2 12937 . . 3  class  <" A B ">
63cs1 12661 . . 3  class  <" C ">
7 cconcat 12660 . . 3  class ++
85, 6, 7co 6304 . 2  class  ( <" A B "> ++  <" C "> )
94, 8wceq 1438 1  wff  <" A B C ">  =  ( <" A B "> ++  <" C "> )
Colors of variables: wff setvar class
This definition is referenced by:  s3eqd  12959  s3cld  12966  s3cli  12975  s3fv0  12984  s3fv1  12985  s3fv2  12986  s3len  12987  s4prop  12998  s3co  13004  s1s2  13006  s1s3  13007  s2s2  13012  s4s3  13014  repsw3  13024  konigsberg  25711
  Copyright terms: Public domain W3C validator