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

Definition df-pgp 16879
 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 16875 . 2 pGrp
2 vp . . . . . . 7
32cv 1404 . . . . . 6
4 cprime 14426 . . . . . 6
53, 4wcel 1842 . . . . 5
6 vg . . . . . . 7
76cv 1404 . . . . . 6
8 cgrp 16377 . . . . . 6
97, 8wcel 1842 . . . . 5
105, 9wa 367 . . . 4
11 vx . . . . . . . . 9
1211cv 1404 . . . . . . . 8
13 cod 16873 . . . . . . . . 9
147, 13cfv 5569 . . . . . . . 8
1512, 14cfv 5569 . . . . . . 7
16 vn . . . . . . . . 9
1716cv 1404 . . . . . . . 8
18 cexp 12210 . . . . . . . 8
193, 17, 18co 6278 . . . . . . 7
2015, 19wceq 1405 . . . . . 6
21 cn0 10836 . . . . . 6
2220, 16, 21wrex 2755 . . . . 5
23 cbs 14841 . . . . . 6
247, 23cfv 5569 . . . . 5
2522, 11, 24wral 2754 . . . 4
2610, 25wa 367 . . 3
2726, 2, 6copab 4452 . 2
281, 27wceq 1405 1 pGrp
 Colors of variables: wff setvar class This definition is referenced by:  ispgp  16936
 Copyright terms: Public domain W3C validator