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

Definition df-reverse 12548
Description: Define an operation which reverses the order of symbols in a word. (Contributed by Stefan O'Rear, 26-Aug-2015.)
Assertion
Ref Expression
df-reverse
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-reverse
StepHypRef Expression
1 creverse 12540 . 2
2 vs . . 3
3 cvv 3109 . . 3
4 vx . . . 4
5 cc0 9513 . . . . 5
62cv 1394 . . . . . 6
7 chash 12405 . . . . . 6
86, 7cfv 5593 . . . . 5
9 cfzo 11824 . . . . 5
105, 8, 9co 6296 . . . 4
11 c1 9514 . . . . . . 7
12 cmin 9828 . . . . . . 7
138, 11, 12co 6296 . . . . . 6
144cv 1394 . . . . . 6
1513, 14, 12co 6296 . . . . 5
1615, 6cfv 5593 . . . 4
174, 10, 16cmpt 4510 . . 3
182, 3, 17cmpt 4510 . 2
191, 18wceq 1395 1
Colors of variables: wff setvar class
This definition is referenced by:  revval  12734
  Copyright terms: Public domain W3C validator