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

Definition df-s2 11514
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 11507 . 2  class  <" A B ">
41cs1 11421 . . 3  class  <" A ">
52cs1 11421 . . 3  class  <" B ">
6 cconcat 11420 . . 3  class concat
74, 5, 6co 5874 . 2  class  ( <" A "> concat  <" B "> )
83, 7wceq 1632 1  wff  <" A B ">  =  (
<" A "> concat  <" B "> )
Colors of variables: wff set class
This definition is referenced by:  s2eqd  11528  s2cld  11535  s2cli  11544  s2fv0  11551  s2fv1  11552  s2len  11553  s2co  11563  s1s2  11566  s2s2  11572  s4s2  11573  swrds2  11576  gsumws2  14481  efginvrel2  15052  efgredlemc  15070  frgpnabllem1  15177  konigsberg  23926  s2prop  28221
  Copyright terms: Public domain W3C validator