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

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

Detailed syntax breakdown of Definition df-s7
StepHypRef Expression
1 cA . . 3
2 cB . . 3
3 cC . . 3
4 cD . . 3
5 cE . . 3
6 cF . . 3
7 cG . . 3
81, 2, 3, 4, 5, 6, 7cs7 12811 . 2
91, 2, 3, 4, 5, 6cs6 12810 . . 3
107cs1 12537 . . 3
11 cconcat 12536 . . 3
129, 10, 11co 6296 . 2
138, 12wceq 1395 1
Colors of variables: wff setvar class
This definition is referenced by:  s7eqd  12832  s7cld  12839  s7cli  12848  s7len  12860  s1s6  12875  s1s7  12876  s4s3  12879  konigsberg  24987
  Copyright terms: Public domain W3C validator