Theorem nzrring 20493

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

Syntax hints:   → wi 4   ∈ wcel 2114   ≠ wne 2932  ‘cfv 6498  0_gc0g 17402  1_rcur 20162  Ringcrg 20214  NzRingcnzr 20489

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-ss 3906  df-nzr 20490

This theorem is referenced by:  nzrunit  20501  lringring  20519  rrgnz  20681  domnring  20684  isdomn4  20693  domnchr  21512  uvcf1  21772  lindfind2  21798  frlmisfrlm  21828  nminvr  24634  deg1pw  26086  ply1nz  26087  mon1pid  26119  ply1remlem  26130  ply1rem  26131  facth1  26132  fta1glem1  26133  fta1glem2  26134  unitnz  33300  drngidl  33493  drngidlhash  33494  prmidl0  33510  drnglidl1ne0  33535  drngmxidlr  33538  krull  33539  qsdrngilem  33554  qsdrngi  33555  qsdrnglem2  33556  qsdrng  33557  ply1moneq  33648  deg1vr  33652  zrhnm  34111  abvexp  42977  uvcn0  42987  0prjspnlem  43056  mon1psubm  43627  nzrneg1ne0  48706  islindeps2  48959