Theorem rnggrp 20078

Description: A non-unital ring is a (additive) group. (Contributed by AV, 16-Feb-2025.)

Assertion

Ref	Expression
rnggrp	⊢ (𝑅 ∈ Rng → 𝑅 ∈ Grp)

Proof of Theorem rnggrp

Step	Hyp	Ref	Expression
1		rngabl 20075	. 2 ⊢ (𝑅 ∈ Rng → 𝑅 ∈ Abel)
2	1	ablgrpd 19700	1 ⊢ (𝑅 ∈ Rng → 𝑅 ∈ Grp)

Syntax hints:   → wi 4   ∈ wcel 2113  Grpcgrp 18848  Rngcrng 20072

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-nul 5246

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ne 2930  df-ral 3049  df-rab 3397  df-v 3439  df-sbc 3738  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-iota 6442  df-fv 6494  df-ov 7355  df-abl 19697  df-rng 20073

This theorem is referenced by:  rngacl  20082  rng0cl  20083  rngrz  20086  rngmneg1  20087  rngmneg2  20088  rngm2neg  20089  rngsubdi  20091  rngsubdir  20092  prdsrngd  20096  subrngsubg  20469  cntzsubrng  20484  rnglidlmcl  21155  rnglidl0  21168  rnglidl1  21171  2idlcpblrng  21210  rngqiprngimfolem  21229  rngqiprngimf1lem  21233  rngqiprngghm  21238  rngqiprngimf1  21239  rngqiprngimfo  21240  rngqiprngfulem3  21252  rngqiprngfulem4  21253  rngqiprngfulem5  21254  pzriprnglem4  21423  pzriprnglem10  21429