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

Definition df-s2 11740
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 11733 . 2  class  <" A B ">
41cs1 11647 . . 3  class  <" A ">
52cs1 11647 . . 3  class  <" B ">
6 cconcat 11646 . . 3  class concat
74, 5, 6co 6021 . 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  11754  s2cld  11761  s2cli  11770  s2fv0  11777  s2fv1  11778  s2len  11779  s2prop  11789  s2co  11795  s1s2  11798  s2s2  11804  s4s2  11805  swrds2  11808  gsumws2  14716  efginvrel2  15287  efgredlemc  15305  frgpnabllem1  15412  konigsberg  21558
  Copyright terms: Public domain W3C validator