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

Definition df-gex 15158
 Description: Define the exponent of a group. (Contributed by Mario Carneiro, 13-Jul-2014.) (Revised by Stefan O'Rear, 4-Sep-2015.)
Assertion
Ref Expression
df-gex gEx .g
Distinct variable group:   ,,,

Detailed syntax breakdown of Definition df-gex
StepHypRef Expression
1 cgex 15154 . 2 gEx
2 vg . . 3
3 cvv 2948 . . 3
4 vi . . . 4
5 vn . . . . . . . . 9
65cv 1651 . . . . . . . 8
7 vx . . . . . . . . 9
87cv 1651 . . . . . . . 8
92cv 1651 . . . . . . . . 9
10 cmg 14679 . . . . . . . . 9 .g
119, 10cfv 5446 . . . . . . . 8 .g
126, 8, 11co 6073 . . . . . . 7 .g
13 c0g 13713 . . . . . . . 8
149, 13cfv 5446 . . . . . . 7
1512, 14wceq 1652 . . . . . 6 .g
16 cbs 13459 . . . . . . 7
179, 16cfv 5446 . . . . . 6
1815, 7, 17wral 2697 . . . . 5 .g
19 cn 9990 . . . . 5
2018, 5, 19crab 2701 . . . 4 .g
214cv 1651 . . . . . 6
22 c0 3620 . . . . . 6
2321, 22wceq 1652 . . . . 5
24 cc0 8980 . . . . 5
25 cr 8979 . . . . . 6
26 clt 9110 . . . . . . 7
2726ccnv 4869 . . . . . 6
2821, 25, 27csup 7437 . . . . 5
2923, 24, 28cif 3731 . . . 4
304, 20, 29csb 3243 . . 3 .g
312, 3, 30cmpt 4258 . 2 .g
321, 31wceq 1652 1 gEx .g
 Colors of variables: wff set class This definition is referenced by:  gexval  15202
 Copyright terms: Public domain W3C validator