Theorem nzrring 20667

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146   ≠ wne 2960  ‘cfv 6540  0_gc0g 17518  1_rcur 20311  Ringcrg 20363  NzRingcnzr 20663

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 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-ss 3923  df-nzr 20664

This theorem is used by:  drnglidl1ne0  20670  nzrunit  20676  lringring  20695  rrgnz  20857  domnring  20860  isdomn4  20868  drngidl  21439  prmidl0  21532  domnchr  21736  uvcf1  21996  lindfind2  22022  frlmisfrlm  22052  nminvr  24881  deg1pw  26333  ply1nz  26334  mon1pid  26366  ply1remlem  26377  ply1rem  26378  facth1  26379  fta1glem1  26380  fta1glem2  26381  unitnz  33626  drngidlhash  33809  drngmxidlr  33828  krull  33829  qsdrngilem  33844  qsdrngi  33845  qsdrnglem2  33846  qsdrng  33847  dflring2  33851  ply1moneq  33946  deg1vr  33950  psrnzr  33970  mplnzr  33971  zrhnm  34425  abvexp  43377  uvcn0  43387  0prjspnlem  43432  mon1psubm  44003  nzrneg1ne0  49071  prmrngring  49179  smprngprmrng  49180  islindeps2  49339