Theorem ablogrpo 30972

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2146  ∀wral 3081  ran crn 5664  (class class class)co 7419  GrpOpcgr 30914  AbelOpcablo 30969

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 2148  ax-9 2156  ax-ext 2737

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 2744  df-cleq 2757  df-clel 2840  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-cnv 5671  df-dm 5673  df-rn 5674  df-iota 6496  df-fv 6548  df-ov 7422  df-ablo 30970

This theorem is used by:  ablo32  30974  ablo4  30975  ablomuldiv  30977  ablodivdiv  30978  ablodivdiv4  30979  ablonncan  30981  ablonnncan1  30982  vcgrp  30995  isvcOLD  31004  isvciOLD  31005  cnidOLD  31007  nvgrp  31042  cnnv  31102  cnnvba  31104  cncph  31244  hilid  31586  hhnv  31590  hhba  31592  hhph  31603  hhssabloilem  31686  hhssnv  31689  ablo4pnp  38591  rngogrpo  38621  iscringd  38709