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

Definition df-gx 25915
 Description: Define a function that maps a group operation to the group's power operation. (Contributed by Paul Chapman, 17-Apr-2009.) (New usage is discouraged.)
Assertion
Ref Expression
df-gx GId
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-gx
StepHypRef Expression
1 cgx 25910 . 2
2 vg . . 3
3 cgr 25906 . . 3
4 vx . . . 4
5 vy . . . 4
62cv 1437 . . . . 5
76crn 4852 . . . 4
8 cz 10939 . . . 4
95cv 1437 . . . . . 6
10 cc0 9541 . . . . . 6
119, 10wceq 1438 . . . . 5
12 cgi 25907 . . . . . 6 GId
136, 12cfv 5599 . . . . 5 GId
14 clt 9677 . . . . . . 7
1510, 9, 14wbr 4421 . . . . . 6
16 cn 10611 . . . . . . . . 9
174cv 1437 . . . . . . . . . 10
1817csn 3997 . . . . . . . . 9
1916, 18cxp 4849 . . . . . . . 8
20 c1 9542 . . . . . . . 8
216, 19, 20cseq 12214 . . . . . . 7
229, 21cfv 5599 . . . . . 6
239cneg 9863 . . . . . . . 8
2423, 21cfv 5599 . . . . . . 7
25 cgn 25908 . . . . . . . 8
266, 25cfv 5599 . . . . . . 7
2724, 26cfv 5599 . . . . . 6
2815, 22, 27cif 3910 . . . . 5
2911, 13, 28cif 3910 . . . 4 GId
304, 5, 7, 8, 29cmpt2 6305 . . 3 GId
312, 3, 30cmpt 4480 . 2 GId
321, 31wceq 1438 1 GId
 Colors of variables: wff setvar class This definition is referenced by:  gxfval  25977
 Copyright terms: Public domain W3C validator