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

Definition df-s2 12770
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 12763 . 2  class  <" A B ">
41cs1 12497 . . 3  class  <" A ">
52cs1 12497 . . 3  class  <" B ">
6 cconcat 12496 . . 3  class concat
74, 5, 6co 6282 . 2  class  ( <" A "> concat  <" B "> )
83, 7wceq 1379 1  wff  <" A B ">  =  (
<" A "> concat  <" B "> )
Colors of variables: wff setvar class
This definition is referenced by:  s2eqd  12784  s2cld  12791  s2cli  12800  s2fv0  12807  s2fv1  12808  s2len  12809  s2prop  12819  s2co  12825  s1s2  12828  s2s2  12834  s4s2  12835  s2eq2s1eq  12838  swrds2  12840  repsw2  12845  ccatw2s1ccatws2  12849  gsumws2  15830  efginvrel2  16538  efgredlemc  16556  frgpnabllem1  16665  konigsberg  24660  ofs2  28138  ofcs2  28139
  Copyright terms: Public domain W3C validator