Theorem nzrring 20702

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 20699	. . 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 2955  ‘cfv 6534  0_gc0g 17546  1_rcur 20343  Ringcrg 20395  NzRingcnzr 20698

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 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-ss 3916  df-nzr 20699

This theorem is used by:  drnglidl1ne0  20705  nzrunit  20711  lringring  20730  rrgnz  20892  domnring  20895  isdomn4  20903  drngidl  21475  prmidl0  21570  domnchr  21774  uvcf1  22034  lindfind2  22060  frlmisfrlm  22090  nminvr  24924  deg1pw  26375  ply1nz  26376  mon1pid  26408  ply1remlem  26419  ply1rem  26420  facth1  26421  fta1glem1  26422  fta1glem2  26423  unitnz  33707  drngidlhash  33891  drngmxidlr  33910  krull  33911  qsdrngilem  33926  qsdrngi  33927  qsdrnglem2  33928  qsdrng  33929  dflring2  33933  ply1moneq  34028  deg1vr  34032  psrnzr  34052  mplnzr  34053  zrhnm  34507  abvexp  43428  uvcn0  43438  0prjspnlem  43483  mon1psubm  44054  nzrneg1ne0  49159  prmrngring  49267  smprngprmrng  49268  islindeps2  49427