Theorem ablogrpo 30899

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

Syntax hints:   → wi 4   = wceq 1570   ∈ wcel 2143  ∀wral 3079  ran crn 5662  (class class class)co 7410  GrpOpcgr 30841  AbelOpcablo 30896

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-cnv 5669  df-dm 5671  df-rn 5672  df-iota 6492  df-fv 6544  df-ov 7413  df-ablo 30897

This theorem is referenced by:  ablo32  30901  ablo4  30902  ablomuldiv  30904  ablodivdiv  30905  ablodivdiv4  30906  ablonncan  30908  ablonnncan1  30909  vcgrp  30922  isvcOLD  30931  isvciOLD  30932  cnidOLD  30934  nvgrp  30969  cnnv  31029  cnnvba  31031  cncph  31171  hilid  31513  hhnv  31517  hhba  31519  hhph  31530  hhssabloilem  31613  hhssnv  31616  ablo4pnp  38551  rngogrpo  38581  iscringd  38669