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 ∈ AbelOp → G ∈ GrpOp

Proof

Step Hyp Ref Expression
1 eqid ⊢ ran ⁡ G = ran ⁡ G
2 1 isablo ⊢ G ∈ AbelOp ↔ G ∈ GrpOp ∧ ∀ x ∈ ran ⁡ G ∀ y ∈ ran ⁡ G x G y = y G x
3 2 simplbi ⊢ G ∈ AbelOp → G ∈ GrpOp