Definition df-subg 8115

Description: Define the set of subgroups of g.

Assertion

Ref	Expression
df-subg	|- SubGrp = {<.g, s>. | (g e. Grp /\ s = {h e. Grp | h (_ g})}

Distinct variable group:   g,h,s

Detailed syntax breakdown of Definition df-subg

Step	Hyp	Ref	Expression
1		csubg 8114	. 2 class SubGrp
2		vg	. . . . . 6 set g
3	2	cv 955	. . . . 5 class g
4		cgr 8033	. . . . 5 class Grp
5	3, 4	wcel 958	. . . 4 wff g e. Grp
6		vs	. . . . . 6 set s
7	6	cv 955	. . . . 5 class s
8		vh	. . . . . . . 8 set h
9	8	cv 955	. . . . . . 7 class h
10	9, 3	wss 2047	. . . . . 6 wff h (_ g
11	10, 8, 4	crab 1648	. . . . 5 class {h e. Grp | h (_ g}
12	7, 11	wceq 956	. . . 4 wff s = {h e. Grp | h (_ g}
13	5, 12	wa 223	. . 3 wff (g e. Grp /\ s = {h e. Grp | h (_ g})
14	13, 2, 6	copab 2666	. 2 class {<.g, s>. | (g e. Grp /\ s = {h e. Grp | h (_ g})}
15	1, 14	wceq 956	1 wff SubGrp = {<.g, s>. | (g e. Grp /\ s = {h e. Grp | h (_ g})}

This definition is referenced by:  issubg 8116

Copyright terms: Public domain