Theorem ablogrpo 28582

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

Syntax hints:   → wi 4   = wceq 1543   ∈ wcel 2112  ∀wral 3051  ran crn 5537  (class class class)co 7191  GrpOpcgr 28524  AbelOpcablo 28579

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-ral 3056  df-rab 3060  df-v 3400  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-nul 4224  df-if 4426  df-sn 4528  df-pr 4530  df-op 4534  df-uni 4806  df-br 5040  df-opab 5102  df-cnv 5544  df-dm 5546  df-rn 5547  df-iota 6316  df-fv 6366  df-ov 7194  df-ablo 28580

This theorem is referenced by:  ablo32  28584  ablo4  28585  ablomuldiv  28587  ablodivdiv  28588  ablodivdiv4  28589  ablonncan  28591  ablonnncan1  28592  vcgrp  28605  isvcOLD  28614  isvciOLD  28615  cnidOLD  28617  nvgrp  28652  cnnv  28712  cnnvba  28714  cncph  28854  hilid  29196  hhnv  29200  hhba  29202  hhph  29213  hhssabloilem  29296  hhssnv  29299  ablo4pnp  35724  rngogrpo  35754  iscringd  35842