Theorem rnggrp 20187

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

Syntax hints:   → wi 4   ∈ wcel 2141  Grpcgrp 18958  Rngcrng 20181

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-nul 5255

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3076  df-rab 3414  df-v 3455  df-sbc 3745  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4480  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-iota 6473  df-fv 6525  df-ov 7395  df-abl 19806  df-rng 20182

This theorem is referenced by:  rngacl  20191  rng0cl  20192  rngrz  20195  rngmneg1  20196  rngmneg2  20197  rngm2neg  20198  rngsubdi  20200  rngsubdir  20201  prdsrngd  20205  subrngsubg  20581  cntzsubrng  20596  rnglidlmcl  21266  rnglidl0  21279  rnglidl1  21282  2idlcpblrng  21321  rngqiprngimfolem  21340  rngqiprngimf1lem  21344  rngqiprngghm  21349  rngqiprngimf1  21350  rngqiprngimfo  21351  rngqiprngfulem3  21363  rngqiprngfulem4  21364  rngqiprngfulem5  21365  pzriprnglem4  21516  pzriprnglem10  21522