Theorem ablogrpo 28888

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2109  ∀wral 3065  ran crn 5589  (class class class)co 7268  GrpOpcgr 28830  AbelOpcablo 28885

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-ral 3070  df-rab 3074  df-v 3432  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-nul 4262  df-if 4465  df-sn 4567  df-pr 4569  df-op 4573  df-uni 4845  df-br 5079  df-opab 5141  df-cnv 5596  df-dm 5598  df-rn 5599  df-iota 6388  df-fv 6438  df-ov 7271  df-ablo 28886

This theorem is referenced by:  ablo32  28890  ablo4  28891  ablomuldiv  28893  ablodivdiv  28894  ablodivdiv4  28895  ablonncan  28897  ablonnncan1  28898  vcgrp  28911  isvcOLD  28920  isvciOLD  28921  cnidOLD  28923  nvgrp  28958  cnnv  29018  cnnvba  29020  cncph  29160  hilid  29502  hhnv  29506  hhba  29508  hhph  29519  hhssabloilem  29602  hhssnv  29605  ablo4pnp  36017  rngogrpo  36047  iscringd  36135