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

Definition df-grpo 21732
 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 21727 . 2
2 vt . . . . . . . 8
32cv 1648 . . . . . . 7
43, 3cxp 4835 . . . . . 6
5 vg . . . . . . 7
65cv 1648 . . . . . 6
74, 3, 6wf 5409 . . . . 5
8 vx . . . . . . . . . . . 12
98cv 1648 . . . . . . . . . . 11
10 vy . . . . . . . . . . . 12
1110cv 1648 . . . . . . . . . . 11
129, 11, 6co 6040 . . . . . . . . . 10
13 vz . . . . . . . . . . 11
1413cv 1648 . . . . . . . . . 10
1512, 14, 6co 6040 . . . . . . . . 9
1611, 14, 6co 6040 . . . . . . . . . 10
179, 16, 6co 6040 . . . . . . . . 9
1815, 17wceq 1649 . . . . . . . 8
1918, 13, 3wral 2666 . . . . . . 7
2019, 10, 3wral 2666 . . . . . 6
2120, 8, 3wral 2666 . . . . 5
22 vu . . . . . . . . . . 11
2322cv 1648 . . . . . . . . . 10
2423, 9, 6co 6040 . . . . . . . . 9
2524, 9wceq 1649 . . . . . . . 8
2611, 9, 6co 6040 . . . . . . . . . 10
2726, 23wceq 1649 . . . . . . . . 9
2827, 10, 3wrex 2667 . . . . . . . 8
2925, 28wa 359 . . . . . . 7
3029, 8, 3wral 2666 . . . . . 6
3130, 22, 3wrex 2667 . . . . 5
327, 21, 31w3a 936 . . . 4
3332, 2wex 1547 . . 3
3433, 5cab 2390 . 2
351, 34wceq 1649 1
 Colors of variables: wff set class This definition is referenced by:  isgrpo  21737
 Copyright terms: Public domain W3C validator