Metamath Proof Explorer

Theorem isabl

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

Ref Expression
Assertion isabl ⊢ G ∈ Abel ↔ G ∈ Grp ∧ G ∈ CMnd

Proof

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