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

Definition df-s2 11767
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 11760 . 2  class  <" A B ">
41cs1 11674 . . 3  class  <" A ">
52cs1 11674 . . 3  class  <" B ">
6 cconcat 11673 . . 3  class concat
74, 5, 6co 6040 . 2  class  ( <" A "> concat  <" B "> )
83, 7wceq 1649 1  wff  <" A B ">  =  (
<" A "> concat  <" B "> )
Colors of variables: wff set class
This definition is referenced by:  s2eqd  11781  s2cld  11788  s2cli  11797  s2fv0  11804  s2fv1  11805  s2len  11806  s2prop  11816  s2co  11822  s1s2  11825  s2s2  11831  s4s2  11832  swrds2  11835  gsumws2  14743  efginvrel2  15314  efgredlemc  15332  frgpnabllem1  15439  konigsberg  21662
  Copyright terms: Public domain W3C validator