Theorem ablogrpo 29197

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

Assertion

Ref	Expression
ablogrpo	⊢ (𝐺 ∈ AbelOp → 𝐺 ∈ GrpOp)

Proof of Theorem ablogrpo

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2736	. . 3 ⊢ ran 𝐺 = ran 𝐺
2	1	isablo 29196	. 2 ⊢ (𝐺 ∈ AbelOp ↔ (𝐺 ∈ GrpOp ∧ ∀𝑥 ∈ ran 𝐺∀𝑦 ∈ ran 𝐺(𝑥𝐺𝑦) = (𝑦𝐺𝑥)))
3	2	simplbi 498	1 ⊢ (𝐺 ∈ AbelOp → 𝐺 ∈ GrpOp)

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2105  ∀wral 3061  ran crn 5621  (class class class)co 7337  GrpOpcgr 29139  AbelOpcablo 29194

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-ral 3062  df-rab 3404  df-v 3443  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4270  df-if 4474  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4853  df-br 5093  df-opab 5155  df-cnv 5628  df-dm 5630  df-rn 5631  df-iota 6431  df-fv 6487  df-ov 7340  df-ablo 29195

This theorem is referenced by:  ablo32  29199  ablo4  29200  ablomuldiv  29202  ablodivdiv  29203  ablodivdiv4  29204  ablonncan  29206  ablonnncan1  29207  vcgrp  29220  isvcOLD  29229  isvciOLD  29230  cnidOLD  29232  nvgrp  29267  cnnv  29327  cnnvba  29329  cncph  29469  hilid  29811  hhnv  29815  hhba  29817  hhph  29828  hhssabloilem  29911  hhssnv  29914  ablo4pnp  36143  rngogrpo  36173  iscringd  36261