Theorem ablogrpo 30575

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 2734	. . 3 ⊢ ran 𝐺 = ran 𝐺
2	1	isablo 30574	. 2 ⊢ (𝐺 ∈ AbelOp ↔ (𝐺 ∈ GrpOp ∧ ∀𝑥 ∈ ran 𝐺∀𝑦 ∈ ran 𝐺(𝑥𝐺𝑦) = (𝑦𝐺𝑥)))
3	2	simplbi 497	1 ⊢ (𝐺 ∈ AbelOp → 𝐺 ∈ GrpOp)

Syntax hints:   → wi 4   = wceq 1536   ∈ wcel 2105  ∀wral 3058  ran crn 5689  (class class class)co 7430  GrpOpcgr 30517  AbelOpcablo 30572

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-cnv 5696  df-dm 5698  df-rn 5699  df-iota 6515  df-fv 6570  df-ov 7433  df-ablo 30573

This theorem is referenced by:  ablo32  30577  ablo4  30578  ablomuldiv  30580  ablodivdiv  30581  ablodivdiv4  30582  ablonncan  30584  ablonnncan1  30585  vcgrp  30598  isvcOLD  30607  isvciOLD  30608  cnidOLD  30610  nvgrp  30645  cnnv  30705  cnnvba  30707  cncph  30847  hilid  31189  hhnv  31193  hhba  31195  hhph  31206  hhssabloilem  31289  hhssnv  31292  ablo4pnp  37866  rngogrpo  37896  iscringd  37984