Theorem nzrring 20453

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

Syntax hints:   → wi 4   ∈ wcel 2114   ≠ wne 2933  ‘cfv 6493  0_gc0g 17363  1_rcur 20120  Ringcrg 20172  NzRingcnzr 20449

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3401  df-ss 3919  df-nzr 20450

This theorem is referenced by:  nzrunit  20461  lringring  20479  rrgnz  20641  domnring  20644  isdomn4  20653  domnchr  21491  uvcf1  21751  lindfind2  21777  frlmisfrlm  21807  nminvr  24617  deg1pw  26086  ply1nz  26087  mon1pid  26119  ply1remlem  26130  ply1rem  26131  facth1  26132  fta1glem1  26133  fta1glem2  26134  unitnz  33323  drngidl  33516  drngidlhash  33517  prmidl0  33533  drnglidl1ne0  33558  drngmxidlr  33561  krull  33562  qsdrngilem  33577  qsdrngi  33578  qsdrnglem2  33579  qsdrng  33580  ply1moneq  33671  deg1vr  33675  zrhnm  34126  abvexp  42854  uvcn0  42864  0prjspnlem  42933  mon1psubm  43508  nzrneg1ne0  48543  islindeps2  48796