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.

Step	Hyp	Ref	Expression
1		df-nzr 20495	. . 3 ⊢ NzRing = {𝑟 ∈ Ring ∣ (1r‘𝑟) ≠ (0g‘𝑟)}
2	1	ssrab3 4079	. 2 ⊢ NzRing ⊆ Ring
3	2	sseli 3975	1 ⊢ (𝑅 ∈ NzRing → 𝑅 ∈ Ring)

Syntax hints:   → wi 4   ∈ wcel 2099   ≠ wne 2930  ‘cfv 6554  0_gc0g 17454  1_rcur 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