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

Definition df-s2 12946
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 12939 . 2  class  <" A B ">
41cs1 12663 . . 3  class  <" A ">
52cs1 12663 . . 3  class  <" B ">
6 cconcat 12662 . . 3  class ++
74, 5, 6co 6305 . 2  class  ( <" A "> ++  <" B "> )
83, 7wceq 1437 1  wff  <" A B ">  =  (
<" A "> ++  <" B "> )
Colors of variables: wff setvar class
This definition is referenced by:  s2eqd  12960  s2cld  12967  s2cli  12976  s2fv0  12983  s2fv1  12984  s2len  12985  s2prop  12999  s2co  13005  s1s2  13008  s2s2  13014  s4s2  13015  s2eq2s1eq  13018  swrds2  13020  repsw2  13025  ccatw2s1ccatws2  13029  gsumws2  16625  efginvrel2  17376  efgredlemc  17394  frgpnabllem1  17508  konigsberg  25713  ofs2  29441  ofcs2  29442
  Copyright terms: Public domain W3C validator