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

Definition df-reverse 11733
 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 11727 . 2 reverse
2 vs . . 3
3 cvv 2958 . . 3
4 vx . . . 4
5 cc0 8995 . . . . 5
62cv 1652 . . . . . 6
7 chash 11623 . . . . . 6
86, 7cfv 5457 . . . . 5
9 cfzo 11140 . . . . 5 ..^
105, 8, 9co 6084 . . . 4 ..^
11 c1 8996 . . . . . . 7
12 cmin 9296 . . . . . . 7
138, 11, 12co 6084 . . . . . 6
144cv 1652 . . . . . 6
1513, 14, 12co 6084 . . . . 5
1615, 6cfv 5457 . . . 4
174, 10, 16cmpt 4269 . . 3 ..^
182, 3, 17cmpt 4269 . 2 ..^
191, 18wceq 1653 1 reverse ..^
 Colors of variables: wff set class This definition is referenced by:  revval  11797
 Copyright terms: Public domain W3C validator