Theorem rnggrp 20092

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

Syntax hints:   → wi 4   ∈ wcel 2099  Grpcgrp 18884  Rngcrng 20086

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 5301

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 2937  df-ral 3058  df-rab 3429  df-v 3472  df-sbc 3776  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-nul 4320  df-if 4526  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4905  df-br 5144  df-iota 6495  df-fv 6551  df-ov 7418  df-abl 19732  df-rng 20087

This theorem is referenced by:  rngacl  20096  rng0cl  20097  rngrz  20100  rngmneg1  20101  rngmneg2  20102  rngm2neg  20103  rngsubdi  20105  rngsubdir  20106  prdsrngd  20110  subrngsubg  20483  cntzsubrng  20498  rnglidlmcl  21106  rnglidl0  21119  rnglidl1  21122  2idlcpblrng  21159  rngqiprngimfolem  21174  rngqiprngimf1lem  21178  rngqiprngghm  21183  rngqiprngimf1  21184  rngqiprngimfo  21185  rngqiprngfulem3  21197  rngqiprngfulem4  21198  rngqiprngfulem5  21199  pzriprnglem4  21404  pzriprnglem10  21410