Theorem nzrring 20542

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

Syntax hints:   → wi 4   ∈ wcel 2108   ≠ wne 2946  ‘cfv 6573  0_gc0g 17499  1_rcur 20208  Ringcrg 20260  NzRingcnzr 20538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-ss 3993  df-nzr 20539

This theorem is referenced by:  nzrunit  20550  lringring  20568  rrgnz  20726  domnring  20729  isdomn4  20738  domnchr  21570  uvcf1  21835  lindfind2  21861  frlmisfrlm  21891  nminvr  24711  deg1pw  26180  ply1nz  26181  mon1pid  26213  ply1remlem  26224  ply1rem  26225  facth1  26226  fta1glem1  26227  fta1glem2  26228  unitnz  33219  drngidl  33426  drngidlhash  33427  prmidl0  33443  drnglidl1ne0  33468  drngmxidlr  33471  krull  33472  qsdrngilem  33487  qsdrngi  33488  qsdrnglem2  33489  qsdrng  33490  ply1moneq  33576  deg1vr  33579  zrhnm  33915  abvexp  42487  uvcn0  42497  0prjspnlem  42578  mon1psubm  43160  nzrneg1ne0  47953  islindeps2  48212