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

Definition df-minusg 14818
 Description: Define inverse of group element. (Contributed by NM, 24-Aug-2011.)
Assertion
Ref Expression
df-minusg
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-minusg
StepHypRef Expression
1 cminusg 14691 . 2
2 vg . . 3
3 cvv 2958 . . 3
4 vx . . . 4
52cv 1652 . . . . 5
6 cbs 13474 . . . . 5
75, 6cfv 5457 . . . 4
8 vw . . . . . . . 8
98cv 1652 . . . . . . 7
104cv 1652 . . . . . . 7
11 cplusg 13534 . . . . . . . 8
125, 11cfv 5457 . . . . . . 7
139, 10, 12co 6084 . . . . . 6
14 c0g 13728 . . . . . . 7
155, 14cfv 5457 . . . . . 6
1613, 15wceq 1653 . . . . 5
1716, 8, 7crio 6545 . . . 4
184, 7, 17cmpt 4269 . . 3
192, 3, 18cmpt 4269 . 2
201, 19wceq 1653 1
 Colors of variables: wff set class This definition is referenced by:  grpinvfval  14848
 Copyright terms: Public domain W3C validator