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

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

Detailed syntax breakdown of Definition df-s5
StepHypRef Expression
1 cA . . 3
2 cB . . 3
3 cC . . 3
4 cD . . 3
5 cE . . 3
61, 2, 3, 4, 5cs5 12809 . 2
71, 2, 3, 4cs4 12808 . . 3
85cs1 12537 . . 3
9 cconcat 12536 . . 3
107, 8, 9co 6296 . 2
116, 10wceq 1395 1
Colors of variables: wff setvar class
This definition is referenced by:  s5eqd  12830  s5cld  12837  s5cli  12846  s5len  12858  s1s4  12873  s1s5  12874  s4s2  12878  konigsberg  24987
  Copyright terms: Public domain W3C validator