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

Definition df-s2 12459
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 12452 . 2  class  <" A B ">
41cs1 12208 . . 3  class  <" A ">
52cs1 12208 . . 3  class  <" B ">
6 cconcat 12207 . . 3  class concat
74, 5, 6co 6080 . 2  class  ( <" A "> concat  <" B "> )
83, 7wceq 1362 1  wff  <" A B ">  =  (
<" A "> concat  <" B "> )
Colors of variables: wff setvar class
This definition is referenced by:  s2eqd  12473  s2cld  12480  s2cli  12489  s2fv0  12496  s2fv1  12497  s2len  12498  s2prop  12508  s2co  12514  s1s2  12517  s2s2  12523  s4s2  12524  s2eq2s1eq  12527  swrds2  12529  repsw2  12534  ccatw2s1ccatws2  12538  gsumws2  15500  efginvrel2  16204  efgredlemc  16222  frgpnabllem1  16331  konigsberg  23431  ofs2  26793  ofcs2  26794
  Copyright terms: Public domain W3C validator