MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nzrring Structured version   Visualization version   GIF version

Theorem nzrring 20498
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.
StepHypRef Expression
1 df-nzr 20495 . . 3 NzRing = {𝑟 ∈ Ring ∣ (1r𝑟) ≠ (0g𝑟)}
21ssrab3 4079 . 2 NzRing ⊆ Ring
32sseli 3975 1 (𝑅 ∈ NzRing → 𝑅 ∈ Ring)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2099  wne 2930  cfv 6554  0gc0g 17454  1rcur 20164  Ringcrg 20216  NzRingcnzr 20494
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697
This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-rab 3420  df-ss 3964  df-nzr 20495
This theorem is referenced by:  nzrunit  20506  lringring  20524  rrgnz  20682  domnring  20685  isdomn4  20694  domnchr  21526  uvcf1  21790  lindfind2  21816  frlmisfrlm  21846  nminvr  24677  deg1pw  26148  ply1nz  26149  mon1pid  26181  ply1remlem  26192  ply1rem  26193  facth1  26194  fta1glem1  26195  fta1glem2  26196  unitnz  33104  drngidl  33308  drngidlhash  33309  prmidl0  33325  drnglidl1ne0  33350  drngmxidlr  33353  krull  33354  qsdrngilem  33369  qsdrngi  33370  qsdrnglem2  33371  qsdrng  33372  ply1moneq  33458  deg1vr  33461  zrhnm  33784  uvcn0  42014  0prjspnlem  42277  mon1psubm  42864  nzrneg1ne0  47607  islindeps2  47866
  Copyright terms: Public domain W3C validator