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	$$⊢\mathrm{Abel}=\mathrm{Grp}\cap \mathrm{CMnd}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cabl	$$class\mathrm{Abel}$$
1		cgrp	$$class\mathrm{Grp}$$
2		ccmn	$$class\mathrm{CMnd}$$
3	1 2	cin	$$class\left(\mathrm{Grp}\cap \mathrm{CMnd}\right)$$
4	0 3	wceq	$$wff\mathrm{Abel}=\mathrm{Grp}\cap \mathrm{CMnd}$$