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

Definition df-s2 12795
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 12788 . 2  class  <" A B ">
41cs1 12519 . . 3  class  <" A ">
52cs1 12519 . . 3  class  <" B ">
6 cconcat 12518 . . 3  class concat
74, 5, 6co 6281 . 2  class  ( <" A "> concat  <" B "> )
83, 7wceq 1383 1  wff  <" A B ">  =  (
<" A "> concat  <" B "> )
Colors of variables: wff setvar class
This definition is referenced by:  s2eqd  12809  s2cld  12816  s2cli  12825  s2fv0  12832  s2fv1  12833  s2len  12834  s2prop  12844  s2co  12850  s1s2  12853  s2s2  12859  s4s2  12860  s2eq2s1eq  12863  swrds2  12865  repsw2  12870  ccatw2s1ccatws2  12874  gsumws2  15989  efginvrel2  16724  efgredlemc  16742  frgpnabllem1  16856  konigsberg  24965  ofs2  28479  ofcs2  28480
  Copyright terms: Public domain W3C validator