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

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

Detailed syntax breakdown of Definition df-s2
StepHypRef Expression
1 cA . . 3  class  A
2 cB . . 3  class  B
31, 2cs2 12460 . 2  class  <" A B ">
41cs1 12216 . . 3  class  <" A ">
52cs1 12216 . . 3  class  <" B ">
6 cconcat 12215 . . 3  class concat
74, 5, 6co 6086 . 2  class  ( <" A "> concat  <" B "> )
83, 7wceq 1369 1  wff  <" A B ">  =  (
<" A "> concat  <" B "> )
Colors of variables: wff setvar class
This definition is referenced by:  s2eqd  12481  s2cld  12488  s2cli  12497  s2fv0  12504  s2fv1  12505  s2len  12506  s2prop  12516  s2co  12522  s1s2  12525  s2s2  12531  s4s2  12532  s2eq2s1eq  12535  swrds2  12537  repsw2  12542  ccatw2s1ccatws2  12546  gsumws2  15511  efginvrel2  16215  efgredlemc  16233  frgpnabllem1  16342  konigsberg  23559  ofs2  26897  ofcs2  26898
  Copyright terms: Public domain W3C validator