Definition df-ablo

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cablo	|- AbelOp
1		vg	|- g
2		cgr	|- GrpOp
3		vx	|- x
4	1	cv	|- g
5	4	crn	|- ran g
6		vy	|- y
7	3	cv	|- x
8	6	cv	|- y
9	7 8 4	co	|- ( x g y )
10	8 7 4	co	|- ( y g x )
11	9 10	wceq	|- ( x g y ) = ( y g x )
12	11 6 5	wral	|- A. y e. ran g ( x g y ) = ( y g x )
13	12 3 5	wral	|- A. x e. ran g A. y e. ran g ( x g y ) = ( y g x )
14	13 1 2	crab	|- { g e. GrpOp | A. x e. ran g A. y e. ran g ( x g y ) = ( y g x ) }
15	0 14	wceq	|- AbelOp = { g e. GrpOp | A. x e. ran g A. y e. ran g ( x g y ) = ( y g x ) }