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

Definition df-reverse 12657
 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 reverse ..^
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-reverse
StepHypRef Expression
1 creverse 12649 . 2 reverse
2 vs . . 3
3 cvv 3087 . . 3
4 vx . . . 4
5 cc0 9538 . . . . 5
62cv 1436 . . . . . 6
7 chash 12512 . . . . . 6
86, 7cfv 5601 . . . . 5
9 cfzo 11913 . . . . 5 ..^
105, 8, 9co 6305 . . . 4 ..^
11 c1 9539 . . . . . . 7
12 cmin 9859 . . . . . . 7
138, 11, 12co 6305 . . . . . 6
144cv 1436 . . . . . 6
1513, 14, 12co 6305 . . . . 5
1615, 6cfv 5601 . . . 4
174, 10, 16cmpt 4484 . . 3 ..^
182, 3, 17cmpt 4484 . 2 ..^
191, 18wceq 1437 1 reverse ..^
 Colors of variables: wff setvar class This definition is referenced by:  revval  12850
 Copyright terms: Public domain W3C validator