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

Definition df-s2 12813
Description: Define the length 2 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.)
Assertion
Ref Expression
df-s2

Detailed syntax breakdown of Definition df-s2
StepHypRef Expression
1 cA . . 3
2 cB . . 3
31, 2cs2 12806 . 2
41cs1 12537 . . 3
52cs1 12537 . . 3
6 cconcat 12536 . . 3
74, 5, 6co 6296 . 2
83, 7wceq 1395 1
Colors of variables: wff setvar class
This definition is referenced by:  s2eqd  12827  s2cld  12834  s2cli  12843  s2fv0  12850  s2fv1  12851  s2len  12852  s2prop  12862  s2co  12868  s1s2  12871  s2s2  12877  s4s2  12878  s2eq2s1eq  12881  swrds2  12883  repsw2  12888  ccatw2s1ccatws2  12892  gsumws2  16010  efginvrel2  16745  efgredlemc  16763  frgpnabllem1  16877  konigsberg  24987  ofs2  28501  ofcs2  28502
  Copyright terms: Public domain W3C validator