Theorem isabl

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

	Ref	Expression
Assertion	isabl	⊢ ( 𝐺 ∈ Abel ↔ ( 𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd ) )

Proof

Step	Hyp	Ref	Expression
1		df-abl	⊢ Abel = ( Grp ∩ CMnd )
2	1	elin2	⊢ ( 𝐺 ∈ Abel ↔ ( 𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd ) )