Definition df-subgo 21882

Description: Define the set of subgroups of g. (Contributed by Paul Chapman, 3-Mar-2008.) (New usage is discouraged.)

Assertion

Ref	Expression
df-subgo	|- SubGrpOp = ( g e. GrpOp |-> ( GrpOp i^i ~P g ) )

Detailed syntax breakdown of Definition df-subgo

Step	Hyp	Ref	Expression
1		csubgo 21881	. 2 class SubGrpOp
2		vg	. . 3 set g
3		cgr 21766	. . 3 class GrpOp
4	2	cv 1651	. . . . 5 class g
5	4	cpw 3791	. . . 4 class ~P g
6	3, 5	cin 3311	. . 3 class ( GrpOp i^i ~P g )
7	2, 3, 6	cmpt 4258	. 2 class ( g e. GrpOp |-> ( GrpOp i^i ~P g ) )
8	1, 7	wceq 1652	1 wff SubGrpOp = ( g e. GrpOp |-> ( GrpOp i^i ~P g ) )

This definition is referenced by:  issubgo  21883