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

Definition df-od 15169
 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 .g
Distinct variable group:   ,,,

Detailed syntax breakdown of Definition df-od
StepHypRef Expression
1 cod 15165 . 2
2 vg . . 3
3 cvv 2958 . . 3
4 vx . . . 4
52cv 1652 . . . . 5
6 cbs 13471 . . . . 5
75, 6cfv 5456 . . . 4
8 vi . . . . 5
9 vn . . . . . . . . 9
109cv 1652 . . . . . . . 8
114cv 1652 . . . . . . . 8
12 cmg 14691 . . . . . . . . 9 .g
135, 12cfv 5456 . . . . . . . 8 .g
1410, 11, 13co 6083 . . . . . . 7 .g
15 c0g 13725 . . . . . . . 8
165, 15cfv 5456 . . . . . . 7
1714, 16wceq 1653 . . . . . 6 .g
18 cn 10002 . . . . . 6
1917, 9, 18crab 2711 . . . . 5 .g
208cv 1652 . . . . . . 7
21 c0 3630 . . . . . . 7
2220, 21wceq 1653 . . . . . 6
23 cc0 8992 . . . . . 6
24 cr 8991 . . . . . . 7
25 clt 9122 . . . . . . . 8
2625ccnv 4879 . . . . . . 7
2720, 24, 26csup 7447 . . . . . 6
2822, 23, 27cif 3741 . . . . 5
298, 19, 28csb 3253 . . . 4 .g
304, 7, 29cmpt 4268 . . 3 .g
312, 3, 30cmpt 4268 . 2 .g
321, 31wceq 1653 1 .g
 Colors of variables: wff set class This definition is referenced by:  odfval  15173
 Copyright terms: Public domain W3C validator