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

Definition df-grpo 21815
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 21810 . 2
2 vt . . . . . . . 8
32cv 1653 . . . . . . 7
43, 3cxp 4921 . . . . . 6
5 vg . . . . . . 7
65cv 1653 . . . . . 6
74, 3, 6wf 5501 . . . . 5
8 vx . . . . . . . . . . . 12
98cv 1653 . . . . . . . . . . 11
10 vy . . . . . . . . . . . 12
1110cv 1653 . . . . . . . . . . 11
129, 11, 6co 6133 . . . . . . . . . 10
13 vz . . . . . . . . . . 11
1413cv 1653 . . . . . . . . . 10
1512, 14, 6co 6133 . . . . . . . . 9
1611, 14, 6co 6133 . . . . . . . . . 10
179, 16, 6co 6133 . . . . . . . . 9
1815, 17wceq 1654 . . . . . . . 8
1918, 13, 3wral 2716 . . . . . . 7
2019, 10, 3wral 2716 . . . . . 6
2120, 8, 3wral 2716 . . . . 5
22 vu . . . . . . . . . . 11
2322cv 1653 . . . . . . . . . 10
2423, 9, 6co 6133 . . . . . . . . 9
2524, 9wceq 1654 . . . . . . . 8
2611, 9, 6co 6133 . . . . . . . . . 10
2726, 23wceq 1654 . . . . . . . . 9
2827, 10, 3wrex 2717 . . . . . . . 8
2925, 28wa 360 . . . . . . 7
3029, 8, 3wral 2716 . . . . . 6
3130, 22, 3wrex 2717 . . . . 5
327, 21, 31w3a 937 . . . 4
3332, 2wex 1551 . . 3
3433, 5cab 2433 . 2
351, 34wceq 1654 1
Colors of variables: wff set class
This definition is referenced by:  isgrpo  21820
  Copyright terms: Public domain W3C validator