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

Definition df-s2 12724
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 12717 . 2  class  <" A B ">
41cs1 12441 . . 3  class  <" A ">
52cs1 12441 . . 3  class  <" B ">
6 cconcat 12440 . . 3  class ++
74, 5, 6co 6196 . 2  class  ( <" A "> ++  <" B "> )
83, 7wceq 1399 1  wff  <" A B ">  =  (
<" A "> ++  <" B "> )
Colors of variables: wff setvar class
This definition is referenced by:  s2eqd  12738  s2cld  12745  s2cli  12754  s2fv0  12761  s2fv1  12762  s2len  12763  s2prop  12773  s2co  12779  s1s2  12782  s2s2  12788  s4s2  12789  s2eq2s1eq  12792  swrds2  12794  repsw2  12799  ccatw2s1ccatws2  12803  gsumws2  16127  efginvrel2  16862  efgredlemc  16880  frgpnabllem1  16994  konigsberg  25108  ofs2  28684  ofcs2  28685
  Copyright terms: Public domain W3C validator