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

Definition df-reps 12549
Description: Definition to construct a word consisting of one repeated symbol, often called "repeated symbol word" for short in the following. (Contributed by Alexander van der Vekens, 4-Nov-2018.)
Assertion
Ref Expression
df-reps
Distinct variable group:   , ,

Detailed syntax breakdown of Definition df-reps
StepHypRef Expression
1 creps 12541 . 2
2 vs . . 3
3 vn . . 3
4 cvv 3109 . . 3
5 cn0 10820 . . 3
6 vx . . . 4
7 cc0 9513 . . . . 5
83cv 1394 . . . . 5
9 cfzo 11824 . . . . 5
107, 8, 9co 6296 . . . 4
112cv 1394 . . . 4
126, 10, 11cmpt 4510 . . 3
132, 3, 4, 5, 12cmpt2 6298 . 2
141, 13wceq 1395 1
Colors of variables: wff setvar class
This definition is referenced by:  reps  12742  repsundef  12743
  Copyright terms: Public domain W3C validator