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

Definition df-s3 11815
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 11808 . 2  class  <" A B C ">
51, 2cs2 11807 . . 3  class  <" A B ">
63cs1 11721 . . 3  class  <" C ">
7 cconcat 11720 . . 3  class concat
85, 6, 7co 6083 . 2  class  ( <" A B "> concat 
<" C "> )
94, 8wceq 1653 1  wff  <" A B C ">  =  ( <" A B "> concat  <" C "> )
Colors of variables: wff set class
This definition is referenced by:  s3eqd  11829  s3cld  11836  s3cli  11845  s3fv0  11854  s3fv1  11855  s3fv2  11856  s3len  11857  s4prop  11864  s3co  11870  s1s2  11872  s1s3  11873  s2s2  11878  s4s3  11880  konigsberg  21711
  Copyright terms: Public domain W3C validator