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

Definition df-pgp 15161
 Description: Define the set of p-groups, which are groups such that every element has a power of as its order. (Contributed by Mario Carneiro, 15-Jan-2015.)
Assertion
Ref Expression
df-pgp pGrp
Distinct variable group:   ,,,

Detailed syntax breakdown of Definition df-pgp
StepHypRef Expression
1 cpgp 15157 . 2 pGrp
2 vp . . . . . . 7
32cv 1651 . . . . . 6
4 cprime 13071 . . . . . 6
53, 4wcel 1725 . . . . 5
6 vg . . . . . . 7
76cv 1651 . . . . . 6
8 cgrp 14677 . . . . . 6
97, 8wcel 1725 . . . . 5
105, 9wa 359 . . . 4
11 vx . . . . . . . . 9
1211cv 1651 . . . . . . . 8
13 cod 15155 . . . . . . . . 9
147, 13cfv 5446 . . . . . . . 8
1512, 14cfv 5446 . . . . . . 7
16 vn . . . . . . . . 9
1716cv 1651 . . . . . . . 8
18 cexp 11374 . . . . . . . 8
193, 17, 18co 6073 . . . . . . 7
2015, 19wceq 1652 . . . . . 6
21 cn0 10213 . . . . . 6
2220, 16, 21wrex 2698 . . . . 5
23 cbs 13461 . . . . . 6
247, 23cfv 5446 . . . . 5
2522, 11, 24wral 2697 . . . 4
2610, 25wa 359 . . 3
2726, 2, 6copab 4257 . 2
281, 27wceq 1652 1 pGrp
 Colors of variables: wff set class This definition is referenced by:  ispgp  15218
 Copyright terms: Public domain W3C validator