Metamath Proof Explorer

Theorem ablogrpo

Description: An Abelian group operation is a group operation. (Contributed by NM, 2-Nov-2006) (New usage is discouraged.)

Ref Expression
Assertion ablogrpo 
|- ( G e. AbelOp -> G e. GrpOp )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ran G = ran G
2 1 isablo 
 |-  ( G e. AbelOp <-> ( G e. GrpOp /\ A. x e. ran G A. y e. ran G ( x G y ) = ( y G x ) ) )
3 2 simplbi 
 |-  ( G e. AbelOp -> G e. GrpOp )