Theorem nzrring 20295

Description: A nonzero ring is a ring. (Contributed by Stefan O'Rear, 24-Feb-2015.) (Proof shortened by SN, 23-Feb-2025.)

Assertion

Ref	Expression
nzrring	⊢ (𝑅 ∈ NzRing → 𝑅 ∈ Ring)

Proof of Theorem nzrring

Dummy variable 𝑟 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-nzr 20292	. . 3 ⊢ NzRing = {𝑟 ∈ Ring ∣ (1r‘𝑟) ≠ (0g‘𝑟)}
2	1	ssrab3 4081	. 2 ⊢ NzRing ⊆ Ring
3	2	sseli 3979	1 ⊢ (𝑅 ∈ NzRing → 𝑅 ∈ Ring)

Syntax hints:   → wi 4   ∈ wcel 2107   ≠ wne 2941  ‘cfv 6544  0_gc0g 17385  1_rcur 20004  Ringcrg 20056  NzRingcnzr 20291

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-in 3956  df-ss 3966  df-nzr 20292

This theorem is referenced by:  opprnzr  20299  nzrunit  20301  lringring  20312  domnring  20912  isdomn4  20918  domnchr  21084  uvcf1  21347  lindfind2  21373  frlmisfrlm  21403  nminvr  24186  deg1pw  25638  ply1nz  25639  ply1remlem  25680  ply1rem  25681  facth1  25682  fta1glem1  25683  fta1glem2  25684  drngidl  32551  drngidlhash  32552  prmidl0  32569  drnglidl1ne0  32591  krull  32594  qsdrngilem  32608  qsdrngi  32609  qsdrnglem2  32610  qsdrng  32611  ply1moneq  32665  zrhnm  32949  uvcn0  41112  0prjspnlem  41365  mon1pid  41947  mon1psubm  41948  nzrneg1ne0  46643  islindeps2  47164