Theorem ablogrpo 30566

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  ∀wral 3061  ran crn 5686  (class class class)co 7431  GrpOpcgr 30508  AbelOpcablo 30563

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-cnv 5693  df-dm 5695  df-rn 5696  df-iota 6514  df-fv 6569  df-ov 7434  df-ablo 30564

This theorem is referenced by:  ablo32  30568  ablo4  30569  ablomuldiv  30571  ablodivdiv  30572  ablodivdiv4  30573  ablonncan  30575  ablonnncan1  30576  vcgrp  30589  isvcOLD  30598  isvciOLD  30599  cnidOLD  30601  nvgrp  30636  cnnv  30696  cnnvba  30698  cncph  30838  hilid  31180  hhnv  31184  hhba  31186  hhph  31197  hhssabloilem  31280  hhssnv  31283  ablo4pnp  37887  rngogrpo  37917  iscringd  38005