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

Theorem nzrring 20516
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 20513 . . 3 NzRing = {𝑟 ∈ Ring ∣ (1r𝑟) ≠ (0g𝑟)}
21ssrab3 4082 . 2 NzRing ⊆ Ring
32sseli 3979 1 (𝑅 ∈ NzRing → 𝑅 ∈ Ring)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2108  wne 2940  cfv 6561  0gc0g 17484  1rcur 20178  Ringcrg 20230  NzRingcnzr 20512
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-ss 3968  df-nzr 20513
This theorem is referenced by:  nzrunit  20524  lringring  20542  rrgnz  20704  domnring  20707  isdomn4  20716  domnchr  21547  uvcf1  21812  lindfind2  21838  frlmisfrlm  21868  nminvr  24690  deg1pw  26160  ply1nz  26161  mon1pid  26193  ply1remlem  26204  ply1rem  26205  facth1  26206  fta1glem1  26207  fta1glem2  26208  unitnz  33243  drngidl  33461  drngidlhash  33462  prmidl0  33478  drnglidl1ne0  33503  drngmxidlr  33506  krull  33507  qsdrngilem  33522  qsdrngi  33523  qsdrnglem2  33524  qsdrng  33525  ply1moneq  33611  deg1vr  33614  zrhnm  33968  abvexp  42542  uvcn0  42552  0prjspnlem  42633  mon1psubm  43211  nzrneg1ne0  48146  islindeps2  48400
  Copyright terms: Public domain W3C validator