Theorem rnggrp 20180

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

Syntax hints:   → wi 4   ∈ wcel 2136  Grpcgrp 18951  Rngcrng 20174

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-8 2138  ax-9 2146  ax-ext 2728  ax-nul 5250

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3an 1097  df-tru 1557  df-fal 1567  df-ex 1794  df-sb 2085  df-clab 2735  df-cleq 2748  df-clel 2831  df-ne 2952  df-ral 3071  df-rab 3409  df-v 3450  df-sbc 3740  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4281  df-if 4475  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5095  df-iota 6466  df-fv 6518  df-ov 7388  df-abl 19799  df-rng 20175

This theorem is referenced by:  rngacl  20184  rng0cl  20185  rngrz  20188  rngmneg1  20189  rngmneg2  20190  rngm2neg  20191  rngsubdi  20193  rngsubdir  20194  prdsrngd  20198  subrngsubg  20574  cntzsubrng  20589  rnglidlmcl  21259  rnglidl0  21272  rnglidl1  21275  2idlcpblrng  21314  rngqiprngimfolem  21333  rngqiprngimf1lem  21337  rngqiprngghm  21342  rngqiprngimf1  21343  rngqiprngimfo  21344  rngqiprngfulem3  21356  rngqiprngfulem4  21357  rngqiprngfulem5  21358  pzriprnglem4  21509  pzriprnglem10  21515