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

Definition df-od 15218
Description: Define the order of an element in a group. (Contributed by Mario Carneiro, 13-Jul-2014.) (Revised by Stefan O'Rear, 4-Sep-2015.)
Assertion
Ref Expression
df-od
Distinct variable group:   , , ,

Detailed syntax breakdown of Definition df-od
StepHypRef Expression
1 cod 15214 . 2
2 vg . . 3
3 cvv 2965 . . 3
4 vx . . . 4
52cv 1653 . . . . 5
6 cbs 13520 . . . . 5
75, 6cfv 5501 . . . 4
8 vi . . . . 5
9 vn . . . . . . . . 9
109cv 1653 . . . . . . . 8
114cv 1653 . . . . . . . 8
12 cmg 14740 . . . . . . . . 9
135, 12cfv 5501 . . . . . . . 8
1410, 11, 13co 6129 . . . . . . 7
15 c0g 13774 . . . . . . . 8
165, 15cfv 5501 . . . . . . 7
1714, 16wceq 1654 . . . . . 6
18 cn 10051 . . . . . 6
1917, 9, 18crab 2716 . . . . 5
208cv 1653 . . . . . . 7
21 c0 3616 . . . . . . 7
2220, 21wceq 1654 . . . . . 6
23 cc0 9041 . . . . . 6
24 cr 9040 . . . . . . 7
25 clt 9171 . . . . . . . 8
2625ccnv 4918 . . . . . . 7
2720, 24, 26csup 7494 . . . . . 6
2822, 23, 27cif 3765 . . . . 5
298, 19, 28csb 3270 . . . 4
304, 7, 29cmpt 4301 . . 3
312, 3, 30cmpt 4301 . 2
321, 31wceq 1654 1
Colors of variables: wff set class
This definition is referenced by:  odfval  15222
  Copyright terms: Public domain W3C validator