Definition df-ablo 27399

Description: Define the class of all Abelian group operations. (Contributed by NM, 2-Nov-2006.) (New usage is discouraged.)

Assertion

Ref	Expression
df-ablo	|- AbelOp = { g e. GrpOp | A. x e. ran g A. y e. ran g ( x g y ) = ( y g x ) }

Distinct variable group:   x, g, y

Detailed syntax breakdown of Definition df-ablo

Step	Hyp	Ref	Expression
1		cablo 27398	. 2 class AbelOp
2		vx	. . . . . . . 8 setvar x
3	2	cv 1482	. . . . . . 7 class x
4		vy	. . . . . . . 8 setvar y
5	4	cv 1482	. . . . . . 7 class y
6		vg	. . . . . . . 8 setvar g
7	6	cv 1482	. . . . . . 7 class g
8	3, 5, 7	co 6650	. . . . . 6 class ( x g y )
9	5, 3, 7	co 6650	. . . . . 6 class ( y g x )
10	8, 9	wceq 1483	. . . . 5 wff ( x g y ) = ( y g x )
11	7	crn 5115	. . . . 5 class ran g
12	10, 4, 11	wral 2912	. . . 4 wff A. y e. ran g ( x g y ) = ( y g x )
13	12, 2, 11	wral 2912	. . 3 wff A. x e. ran g A. y e. ran g ( x g y ) = ( y g x )
14		cgr 27343	. . 3 class GrpOp
15	13, 6, 14	crab 2916	. 2 class { g e. GrpOp | A. x e. ran g A. y e. ran g ( x g y ) = ( y g x ) }
16	1, 15	wceq 1483	1 wff AbelOp = { g e. GrpOp | A. x e. ran g A. y e. ran g ( x g y ) = ( y g x ) }

This definition is referenced by:  isablo  27400