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 ∩ CMnd )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cabl	⊢ Abel
1		cgrp	⊢ Grp
2		ccmn	⊢ CMnd
3	1 2	cin	⊢ ( Grp ∩ CMnd )
4	0 3	wceq	⊢ Abel = ( Grp ∩ CMnd )