Theorem ablogrpo 31031

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  ∀wral 3076  ran crn 5656  (class class class)co 7414  GrpOpcgr 30973  AbelOpcablo 31028

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-cnv 5663  df-dm 5665  df-rn 5666  df-iota 6489  df-fv 6541  df-ov 7417  df-ablo 31029

This theorem is used by:  ablo32  31033  ablo4  31034  ablomuldiv  31036  ablodivdiv  31037  ablodivdiv4  31038  ablonncan  31040  ablonnncan1  31041  vcgrp  31054  isvcOLD  31063  isvciOLD  31064  cnidOLD  31066  nvgrp  31101  cnnv  31161  cnnvba  31163  cncph  31303  hilid  31645  hhnv  31649  hhba  31651  hhph  31662  hhssabloilem  31745  hhssnv  31748  ablo4pnp  38633  rngogrpo  38663  iscringd  38751