Theorem nzrring 20599

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 20596	. . 3 ⊢ NzRing = {𝑟 ∈ Ring ∣ (1r‘𝑟) ≠ (0g‘𝑟)}
2	1	ssrab3 4044	. 2 ⊢ NzRing ⊆ Ring
3	2	sseli 3941	1 ⊢ (𝑅 ∈ NzRing → 𝑅 ∈ Ring)

Syntax hints:   → wi 4   ∈ wcel 2149   ≠ wne 2964  ‘cfv 6537  0_gc0g 17492  1_rcur 20263  Ringcrg 20315  NzRingcnzr 20595

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-ss 3930  df-nzr 20596

This theorem is referenced by:  drnglidl1ne0  20602  nzrunit  20608  lringring  20627  rrgnz  20789  domnring  20792  isdomn4  20800  prmidl0  21447  domnchr  21651  uvcf1  21911  lindfind2  21937  frlmisfrlm  21967  nminvr  24795  deg1pw  26247  ply1nz  26248  mon1pid  26280  ply1remlem  26291  ply1rem  26292  facth1  26293  fta1glem1  26294  fta1glem2  26295  unitnz  33499  drngidl  33685  drngidlhash  33686  drngmxidlr  33705  krull  33706  qsdrngilem  33721  qsdrngi  33722  qsdrnglem2  33723  qsdrng  33724  dflring2  33728  ply1moneq  33823  deg1vr  33827  psrnzr  33847  mplnzr  33848  zrhnm  34302  abvexp  43226  uvcn0  43236  0prjspnlem  43281  mon1psubm  43852  nzrneg1ne0  48918  prmrngring  49026  smprngprmrng  49027  islindeps2  49182