Theorem rnggrp 20185

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

Syntax hints:   → wi 4   ∈ wcel 2108  Grpcgrp 18973  Rngcrng 20179

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-nul 5324

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ne 2947  df-ral 3068  df-rab 3444  df-v 3490  df-sbc 3805  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-iota 6525  df-fv 6581  df-ov 7451  df-abl 19825  df-rng 20180

This theorem is referenced by:  rngacl  20189  rng0cl  20190  rngrz  20193  rngmneg1  20194  rngmneg2  20195  rngm2neg  20196  rngsubdi  20198  rngsubdir  20199  prdsrngd  20203  subrngsubg  20578  cntzsubrng  20593  rnglidlmcl  21249  rnglidl0  21262  rnglidl1  21265  2idlcpblrng  21304  rngqiprngimfolem  21323  rngqiprngimf1lem  21327  rngqiprngghm  21332  rngqiprngimf1  21333  rngqiprngimfo  21334  rngqiprngfulem3  21346  rngqiprngfulem4  21347  rngqiprngfulem5  21348  pzriprnglem4  21518  pzriprnglem10  21524