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

Definition df-grpo 21772
 Description: Define the class of all group operations. The base set for a group can be determined from its group operation. Based on the definition in Exercise 28 of [Herstein] p. 54. (Contributed by NM, 10-Oct-2006.) (New usage is discouraged.)
Assertion
Ref Expression
df-grpo
Distinct variable group:   ,,,,,

Detailed syntax breakdown of Definition df-grpo
StepHypRef Expression
1 cgr 21767 . 2
2 vt . . . . . . . 8
32cv 1651 . . . . . . 7
43, 3cxp 4869 . . . . . 6
5 vg . . . . . . 7
65cv 1651 . . . . . 6
74, 3, 6wf 5443 . . . . 5
8 vx . . . . . . . . . . . 12
98cv 1651 . . . . . . . . . . 11
10 vy . . . . . . . . . . . 12
1110cv 1651 . . . . . . . . . . 11
129, 11, 6co 6074 . . . . . . . . . 10
13 vz . . . . . . . . . . 11
1413cv 1651 . . . . . . . . . 10
1512, 14, 6co 6074 . . . . . . . . 9
1611, 14, 6co 6074 . . . . . . . . . 10
179, 16, 6co 6074 . . . . . . . . 9
1815, 17wceq 1652 . . . . . . . 8
1918, 13, 3wral 2698 . . . . . . 7
2019, 10, 3wral 2698 . . . . . 6
2120, 8, 3wral 2698 . . . . 5
22 vu . . . . . . . . . . 11
2322cv 1651 . . . . . . . . . 10
2423, 9, 6co 6074 . . . . . . . . 9
2524, 9wceq 1652 . . . . . . . 8
2611, 9, 6co 6074 . . . . . . . . . 10
2726, 23wceq 1652 . . . . . . . . 9
2827, 10, 3wrex 2699 . . . . . . . 8
2925, 28wa 359 . . . . . . 7
3029, 8, 3wral 2698 . . . . . 6
3130, 22, 3wrex 2699 . . . . 5
327, 21, 31w3a 936 . . . 4
3332, 2wex 1550 . . 3
3433, 5cab 2422 . 2
351, 34wceq 1652 1
 Colors of variables: wff set class This definition is referenced by:  isgrpo  21777
 Copyright terms: Public domain W3C validator