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

Definition df-s2 12987
Description: Define the length 2 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.)
Assertion
Ref Expression
df-s2  |-  <" A B ">  =  (
<" A "> ++  <" B "> )

Detailed syntax breakdown of Definition df-s2
StepHypRef Expression
1 cA . . 3  class  A
2 cB . . 3  class  B
31, 2cs2 12980 . 2  class  <" A B ">
41cs1 12698 . . 3  class  <" A ">
52cs1 12698 . . 3  class  <" B ">
6 cconcat 12697 . . 3  class ++
74, 5, 6co 6320 . 2  class  ( <" A "> ++  <" B "> )
83, 7wceq 1455 1  wff  <" A B ">  =  (
<" A "> ++  <" B "> )
Colors of variables: wff setvar class
This definition is referenced by:  s2eqd  13001  s2cld  13008  s2cli  13017  s2fv0  13024  s2fv1  13025  s2len  13026  s2prop  13044  s2co  13057  s1s2  13060  s2s2  13066  s4s2  13067  s2eq2s1eq  13070  swrds2  13072  repsw2  13080  ccatw2s1ccatws2  13084  gsumws2  16681  efginvrel2  17432  efgredlemc  17450  frgpnabllem1  17564  konigsberg  25771  ofs2  29483  ofcs2  29484  2pthon3v-av  39988
  Copyright terms: Public domain W3C validator