Theorem nzrring 20401

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

Syntax hints:   → wi 4   ∈ wcel 2109   ≠ wne 2925  ‘cfv 6482  0_gc0g 17343  1_rcur 20066  Ringcrg 20118  NzRingcnzr 20397

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3395  df-ss 3920  df-nzr 20398

This theorem is referenced by:  nzrunit  20409  lringring  20427  rrgnz  20589  domnring  20592  isdomn4  20601  domnchr  21439  uvcf1  21699  lindfind2  21725  frlmisfrlm  21755  nminvr  24555  deg1pw  26024  ply1nz  26025  mon1pid  26057  ply1remlem  26068  ply1rem  26069  facth1  26070  fta1glem1  26071  fta1glem2  26072  unitnz  33188  drngidl  33379  drngidlhash  33380  prmidl0  33396  drnglidl1ne0  33421  drngmxidlr  33424  krull  33425  qsdrngilem  33440  qsdrngi  33441  qsdrnglem2  33442  qsdrng  33443  ply1moneq  33531  deg1vr  33534  zrhnm  33950  abvexp  42525  uvcn0  42535  0prjspnlem  42616  mon1psubm  43192  nzrneg1ne0  48234  islindeps2  48488