Theorem ablogrpo 30491

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  ∀wral 3044  ran crn 5620  (class class class)co 7349  GrpOpcgr 30433  AbelOpcablo 30488

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-cnv 5627  df-dm 5629  df-rn 5630  df-iota 6438  df-fv 6490  df-ov 7352  df-ablo 30489

This theorem is referenced by:  ablo32  30493  ablo4  30494  ablomuldiv  30496  ablodivdiv  30497  ablodivdiv4  30498  ablonncan  30500  ablonnncan1  30501  vcgrp  30514  isvcOLD  30523  isvciOLD  30524  cnidOLD  30526  nvgrp  30561  cnnv  30621  cnnvba  30623  cncph  30763  hilid  31105  hhnv  31109  hhba  31111  hhph  31122  hhssabloilem  31205  hhssnv  31208  ablo4pnp  37870  rngogrpo  37900  iscringd  37988