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

Definition df-s2 11498
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 11491 . 2  class  <" A B ">
41cs1 11405 . . 3  class  <" A ">
52cs1 11405 . . 3  class  <" B ">
6 cconcat 11404 . . 3  class concat
74, 5, 6co 5858 . 2  class  ( <" A "> concat  <" B "> )
83, 7wceq 1623 1  wff  <" A B ">  =  (
<" A "> concat  <" B "> )
Colors of variables: wff set class
This definition is referenced by:  s2eqd  11512  s2cld  11519  s2cli  11528  s2fv0  11535  s2fv1  11536  s2len  11537  s2co  11547  s1s2  11550  s2s2  11556  s4s2  11557  swrds2  11560  gsumws2  14465  efginvrel2  15036  efgredlemc  15054  frgpnabllem1  15161  konigsberg  23911  s2prop  28089
  Copyright terms: Public domain W3C validator