Theorem nzrring 20492

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

Syntax hints:   → wi 4   ∈ wcel 2121   ≠ wne 2936  ‘cfv 6489  0_gc0g 17397  1_rcur 20157  Ringcrg 20209  NzRingcnzr 20488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-rab 3394  df-ss 3902  df-nzr 20489

This theorem is referenced by:  nzrunit  20500  lringring  20518  rrgnz  20680  domnring  20683  isdomn4  20692  domnchr  21511  uvcf1  21771  lindfind2  21797  frlmisfrlm  21827  nminvr  24656  deg1pw  26108  ply1nz  26109  mon1pid  26141  ply1remlem  26152  ply1rem  26153  facth1  26154  fta1glem1  26155  fta1glem2  26156  unitnz  33324  drngidl  33520  drngidlhash  33521  prmidl0  33537  drnglidl1ne0  33562  drngmxidlr  33565  krull  33566  qsdrngilem  33581  qsdrngi  33582  qsdrnglem2  33583  qsdrng  33584  dflring2  33588  ply1moneq  33683  deg1vr  33687  psrnzr  33708  mplnzr  33709  zrhnm  34163  abvexp  43033  uvcn0  43043  0prjspnlem  43088  mon1psubm  43659  nzrneg1ne0  48735  islindeps2  48988