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  33180  drngidl  33371  drngidlhash  33372  prmidl0  33388  drnglidl1ne0  33413  drngmxidlr  33416  krull  33417  qsdrngilem  33432  qsdrngi  33433  qsdrnglem2  33434  qsdrng  33435  ply1moneq  33523  deg1vr  33526  zrhnm  33940  abvexp  42515  uvcn0  42525  0prjspnlem  42606  mon1psubm  43182  nzrneg1ne0  48224  islindeps2  48478