Theorem rnggrp 20130

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

Syntax hints:   → wi 4   ∈ wcel 2114  Grpcgrp 18900  Rngcrng 20124

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-nul 5241

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rab 3391  df-v 3432  df-sbc 3730  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6448  df-fv 6500  df-ov 7363  df-abl 19749  df-rng 20125

This theorem is referenced by:  rngacl  20134  rng0cl  20135  rngrz  20138  rngmneg1  20139  rngmneg2  20140  rngm2neg  20141  rngsubdi  20143  rngsubdir  20144  prdsrngd  20148  subrngsubg  20520  cntzsubrng  20535  rnglidlmcl  21206  rnglidl0  21219  rnglidl1  21222  2idlcpblrng  21261  rngqiprngimfolem  21280  rngqiprngimf1lem  21284  rngqiprngghm  21289  rngqiprngimf1  21290  rngqiprngimfo  21291  rngqiprngfulem3  21303  rngqiprngfulem4  21304  rngqiprngfulem5  21305  pzriprnglem4  21474  pzriprnglem10  21480