Theorem rnggrp 20098

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

Syntax hints:   → wi 4   ∈ wcel 2099  Grpcgrp 18890  Rngcrng 20092

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699  ax-nul 5306

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-ne 2938  df-ral 3059  df-rab 3430  df-v 3473  df-sbc 3777  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-br 5149  df-iota 6500  df-fv 6556  df-ov 7423  df-abl 19738  df-rng 20093

This theorem is referenced by:  rngacl  20102  rng0cl  20103  rngrz  20106  rngmneg1  20107  rngmneg2  20108  rngm2neg  20109  rngsubdi  20111  rngsubdir  20112  prdsrngd  20116  subrngsubg  20489  cntzsubrng  20504  rnglidlmcl  21112  rnglidl0  21125  rnglidl1  21128  2idlcpblrng  21165  rngqiprngimfolem  21180  rngqiprngimf1lem  21184  rngqiprngghm  21189  rngqiprngimf1  21190  rngqiprngimfo  21191  rngqiprngfulem3  21203  rngqiprngfulem4  21204  rngqiprngfulem5  21205  pzriprnglem4  21410  pzriprnglem10  21416