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

Definition df-s2 11804
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 11797 . 2  class  <" A B ">
41cs1 11711 . . 3  class  <" A ">
52cs1 11711 . . 3  class  <" B ">
6 cconcat 11710 . . 3  class concat
74, 5, 6co 6073 . 2  class  ( <" A "> concat  <" B "> )
83, 7wceq 1652 1  wff  <" A B ">  =  (
<" A "> concat  <" B "> )
Colors of variables: wff set class
This definition is referenced by:  s2eqd  11818  s2cld  11825  s2cli  11834  s2fv0  11841  s2fv1  11842  s2len  11843  s2prop  11853  s2co  11859  s1s2  11862  s2s2  11868  s4s2  11869  swrds2  11872  gsumws2  14780  efginvrel2  15351  efgredlemc  15369  frgpnabllem1  15476  konigsberg  21701
  Copyright terms: Public domain W3C validator