Definition df-abl 8100

Description: Define the class of all Abelian group operations.

Assertion

Ref	Expression
df-abl	|- Abel = {g e. Grp | A.x e. ran gA.y e. ran g(xgy) = (ygx)}

Distinct variable group:   x,g,y

Detailed syntax breakdown of Definition df-abl

Step	Hyp	Ref	Expression
1		cabl 8099	. 2 class Abel
2		vx	. . . . . . . 8 set x
3	2	cv 955	. . . . . . 7 class x
4		vy	. . . . . . . 8 set y
5	4	cv 955	. . . . . . 7 class y
6		vg	. . . . . . . 8 set g
7	6	cv 955	. . . . . . 7 class g
8	3, 5, 7	co 3963	. . . . . 6 class (xgy)
9	5, 3, 7	co 3963	. . . . . 6 class (ygx)
10	8, 9	wceq 956	. . . . 5 wff (xgy) = (ygx)
11	7	crn 3171	. . . . 5 class ran g
12	10, 4, 11	wral 1645	. . . 4 wff A.y e. ran g(xgy) = (ygx)
13	12, 2, 11	wral 1645	. . 3 wff A.x e. ran gA.y e. ran g(xgy) = (ygx)
14		cgr 8033	. . 3 class Grp
15	13, 6, 14	crab 1648	. 2 class {g e. Grp | A.x e. ran gA.y e. ran g(xgy) = (ygx)}
16	1, 15	wceq 956	1 wff Abel = {g e. Grp | A.x e. ran gA.y e. ran g(xgy) = (ygx)}

This definition is referenced by:  isabl 8101

Copyright terms: Public domain