Theorem nzrring 20766

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   ≠ wne 2956  ‘cfv 6538  0_gc0g 17610  1_rcur 20407  Ringcrg 20459  NzRingcnzr 20762

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-ss 3916  df-nzr 20763

This theorem is used by:  drnglidl1ne0  20769  nzrunit  20775  lringring  20794  rrgnz  20956  domnring  20959  isdomn4  20967  drngidl  21539  prmidl0  21634  domnchr  21838  uvcf1  22098  lindfind2  22124  frlmisfrlm  22154  nminvr  24988  deg1pw  26439  ply1nz  26440  mon1pid  26472  ply1remlem  26483  ply1rem  26484  facth1  26485  fta1glem1  26486  fta1glem2  26487  unitnz  33799  drngidlhash  33983  drngmxidlr  34002  krull  34003  qsdrngilem  34018  qsdrngi  34019  qsdrnglem2  34020  qsdrng  34021  dflring2  34025  ply1moneq  34120  deg1vr  34124  psrnzr  34144  mplnzr  34145  zrhnm  34599  abvexp  43596  uvcn0  43606  0prjspnlem  43662  mon1psubm  44200  nzrneg1ne0  49326  prmrngring  49434  smprngprmrng  49435  islindeps2  49594