Theorem ablogrpo 30636

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

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119  ∀wral 3053  ran crn 5619  (class class class)co 7356  GrpOpcgr 30578  AbelOpcablo 30633

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-opab 5135  df-cnv 5626  df-dm 5628  df-rn 5629  df-iota 6441  df-fv 6493  df-ov 7359  df-ablo 30634

This theorem is referenced by:  ablo32  30638  ablo4  30639  ablomuldiv  30641  ablodivdiv  30642  ablodivdiv4  30643  ablonncan  30645  ablonnncan1  30646  vcgrp  30659  isvcOLD  30668  isvciOLD  30669  cnidOLD  30671  nvgrp  30706  cnnv  30766  cnnvba  30768  cncph  30908  hilid  31250  hhnv  31254  hhba  31256  hhph  31267  hhssabloilem  31350  hhssnv  31353  ablo4pnp  38247  rngogrpo  38277  iscringd  38365