Metamath Proof Explorer

Theorem isabl

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

Ref Expression
Assertion isabl 
|- ( G e. Abel <-> ( G e. Grp /\ G e. CMnd ) )

Proof

Step Hyp Ref Expression
1 df-abl 
 |-  Abel = ( Grp i^i CMnd )
2 1 elin2 
 |-  ( G e. Abel <-> ( G e. Grp /\ G e. CMnd ) )