Definition df-abl

Description: Define class of all Abelian groups. (Contributed by NM, 17-Oct-2011) (Revised by Mario Carneiro, 6-Jan-2015)

	Ref	Expression
Assertion	df-abl	|- Abel = ( Grp i^i CMnd )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cabl	|- Abel
1		cgrp	|- Grp
2		ccmn	|- CMnd
3	1 2	cin	|- ( Grp i^i CMnd )
4	0 3	wceq	|- Abel = ( Grp i^i CMnd )