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

Definition df-s2 12929
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 12922 . 2  class  <" A B ">
41cs1 12646 . . 3  class  <" A ">
52cs1 12646 . . 3  class  <" B ">
6 cconcat 12645 . . 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  12943  s2cld  12950  s2cli  12959  s2fv0  12966  s2fv1  12967  s2len  12968  s2prop  12978  s2co  12984  s1s2  12987  s2s2  12993  s4s2  12994  s2eq2s1eq  12997  swrds2  12999  repsw2  13004  ccatw2s1ccatws2  13008  gsumws2  16577  efginvrel2  17312  efgredlemc  17330  frgpnabllem1  17444  konigsberg  25560  ofs2  29221  ofcs2  29222
  Copyright terms: Public domain W3C validator