Theorem rnggrp 20074

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 20071	. 2 ⊢ (𝑅 ∈ Rng → 𝑅 ∈ Abel)
2	1	ablgrpd 19696	1 ⊢ (𝑅 ∈ Rng → 𝑅 ∈ Grp)

Syntax hints:   → wi 4   ∈ wcel 2111  Grpcgrp 18843  Rngcrng 20068

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 2113  ax-9 2121  ax-ext 2703  ax-nul 5244

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 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-ral 3048  df-rab 3396  df-v 3438  df-sbc 3742  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5092  df-iota 6437  df-fv 6489  df-ov 7349  df-abl 19693  df-rng 20069

This theorem is referenced by:  rngacl  20078  rng0cl  20079  rngrz  20082  rngmneg1  20083  rngmneg2  20084  rngm2neg  20085  rngsubdi  20087  rngsubdir  20088  prdsrngd  20092  subrngsubg  20465  cntzsubrng  20480  rnglidlmcl  21151  rnglidl0  21164  rnglidl1  21167  2idlcpblrng  21206  rngqiprngimfolem  21225  rngqiprngimf1lem  21229  rngqiprngghm  21234  rngqiprngimf1  21235  rngqiprngimfo  21236  rngqiprngfulem3  21248  rngqiprngfulem4  21249  rngqiprngfulem5  21250  pzriprnglem4  21419  pzriprnglem10  21425