Theorem isabl

Description: The predicate "is an Abelian (commutative) group." (Contributed by NM, 17-Oct-2011)

	Ref	Expression
Assertion	isabl	$$⊢G\in \mathrm{Abel}\leftrightarrow \left(G\in \mathrm{Grp}\wedge G\in \mathrm{CMnd}\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-abl	$$⊢\mathrm{Abel}=\mathrm{Grp}\cap \mathrm{CMnd}$$
2	1	elin2	$$⊢G\in \mathrm{Abel}\leftrightarrow \left(G\in \mathrm{Grp}\wedge G\in \mathrm{CMnd}\right)$$