Theorem nzrring 20431

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

Syntax hints:   → wi 4   ∈ wcel 2111   ≠ wne 2928  ‘cfv 6481  0_gc0g 17343  1_rcur 20099  Ringcrg 20151  NzRingcnzr 20427

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-ss 3914  df-nzr 20428

This theorem is referenced by:  nzrunit  20439  lringring  20457  rrgnz  20619  domnring  20622  isdomn4  20631  domnchr  21469  uvcf1  21729  lindfind2  21755  frlmisfrlm  21785  nminvr  24584  deg1pw  26053  ply1nz  26054  mon1pid  26086  ply1remlem  26097  ply1rem  26098  facth1  26099  fta1glem1  26100  fta1glem2  26101  unitnz  33206  drngidl  33398  drngidlhash  33399  prmidl0  33415  drnglidl1ne0  33440  drngmxidlr  33443  krull  33444  qsdrngilem  33459  qsdrngi  33460  qsdrnglem2  33461  qsdrng  33462  ply1moneq  33550  deg1vr  33553  zrhnm  33980  abvexp  42624  uvcn0  42634  0prjspnlem  42715  mon1psubm  43291  nzrneg1ne0  48329  islindeps2  48583