Theorem ablogrpo 30750

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

Syntax hints:   → wi 4   = wceq 1560   ∈ wcel 2142  ∀wral 3076  ran crn 5648  (class class class)co 7396  GrpOpcgr 30692  AbelOpcablo 30747

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3077  df-rex 3087  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-cnv 5655  df-dm 5657  df-rn 5658  df-iota 6477  df-fv 6529  df-ov 7399  df-ablo 30748

This theorem is referenced by:  ablo32  30752  ablo4  30753  ablomuldiv  30755  ablodivdiv  30756  ablodivdiv4  30757  ablonncan  30759  ablonnncan1  30760  vcgrp  30773  isvcOLD  30782  isvciOLD  30783  cnidOLD  30785  nvgrp  30820  cnnv  30880  cnnvba  30882  cncph  31022  hilid  31364  hhnv  31368  hhba  31370  hhph  31381  hhssabloilem  31464  hhssnv  31467  ablo4pnp  38379  rngogrpo  38409  iscringd  38497