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

Definition df-s2 12594
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 12587 . 2  class  <" A B ">
41cs1 12343 . . 3  class  <" A ">
52cs1 12343 . . 3  class  <" B ">
6 cconcat 12342 . . 3  class concat
74, 5, 6co 6201 . 2  class  ( <" A "> concat  <" B "> )
83, 7wceq 1370 1  wff  <" A B ">  =  (
<" A "> concat  <" B "> )
Colors of variables: wff setvar class
This definition is referenced by:  s2eqd  12608  s2cld  12615  s2cli  12624  s2fv0  12631  s2fv1  12632  s2len  12633  s2prop  12643  s2co  12649  s1s2  12652  s2s2  12658  s4s2  12659  s2eq2s1eq  12662  swrds2  12664  repsw2  12669  ccatw2s1ccatws2  12673  gsumws2  15640  efginvrel2  16346  efgredlemc  16364  frgpnabllem1  16473  konigsberg  23761  ofs2  27090  ofcs2  27091
  Copyright terms: Public domain W3C validator