Theorem ablogrpo 30622

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  ∀wral 3051  ran crn 5625  (class class class)co 7358  GrpOpcgr 30564  AbelOpcablo 30619

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 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-cnv 5632  df-dm 5634  df-rn 5635  df-iota 6448  df-fv 6500  df-ov 7361  df-ablo 30620

This theorem is referenced by:  ablo32  30624  ablo4  30625  ablomuldiv  30627  ablodivdiv  30628  ablodivdiv4  30629  ablonncan  30631  ablonnncan1  30632  vcgrp  30645  isvcOLD  30654  isvciOLD  30655  cnidOLD  30657  nvgrp  30692  cnnv  30752  cnnvba  30754  cncph  30894  hilid  31236  hhnv  31240  hhba  31242  hhph  31253  hhssabloilem  31336  hhssnv  31339  ablo4pnp  38081  rngogrpo  38111  iscringd  38199