Theorem nzrring 20793

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147   ≠ wne 2959  ‘cfv 6555  0_gc0g 17636  1_rcur 20434  Ringcrg 20486  NzRingcnzr 20789

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-ss 3901  df-nzr 20790

This theorem is used by:  drnglidl1ne0  20796  nzrunit  20802  lringring  20821  rrgnz  20983  domnring  20986  isdomn4  20994  drngidl  21566  prmidl0  21661  domnchr  21865  uvcf1  22125  lindfind2  22151  frlmisfrlm  22181  nminvr  25015  deg1pw  26466  ply1nz  26467  mon1pid  26499  ply1remlem  26510  ply1rem  26511  facth1  26512  fta1glem1  26513  fta1glem2  26514  unitnz  33866  drngidlhash  34050  drngmxidlr  34069  krull  34070  qsdrngilem  34085  qsdrngi  34086  qsdrnglem2  34087  qsdrng  34088  dflring2  34092  ply1moneq  34187  deg1vr  34191  psrnzr  34211  mplnzr  34212  zrhnm  34666  abvexp  43787  uvcn0  43797  0prjspnlem  43853  mon1psubm  44391  nzrneg1ne0  49530  prmrngring  49638  smprngprmrng  49639  islindeps2  49798