Theorem ablogrpo 31164

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2146  ∀wral 3080  ran crn 5656  (class class class)co 7430  GrpOpcgr 31106  AbelOpcablo 31161

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-cnv 5663  df-dm 5665  df-rn 5666  df-iota 6501  df-fv 6555  df-ov 7433  df-ablo 31162

This theorem is used by:  ablo32  31166  ablo4  31167  ablomuldiv  31169  ablodivdiv  31170  ablodivdiv4  31171  ablonncan  31173  ablonnncan1  31174  vcgrp  31187  isvcOLD  31196  isvciOLD  31197  cnidOLD  31199  nvgrp  31234  cnnv  31294  cnnvba  31296  cncph  31436  hilid  31778  hhnv  31782  hhba  31784  hhph  31795  hhssabloilem  31878  hhssnv  31881  ablo4pnp  38957  rngogrpo  38987  iscringd  39075