Theorem nzrring 20432

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

Syntax hints:   → wi 4   ∈ wcel 2109   ≠ wne 2926  ‘cfv 6514  0_gc0g 17409  1_rcur 20097  Ringcrg 20149  NzRingcnzr 20428

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-ss 3934  df-nzr 20429

This theorem is referenced by:  nzrunit  20440  lringring  20458  rrgnz  20620  domnring  20623  isdomn4  20632  domnchr  21449  uvcf1  21708  lindfind2  21734  frlmisfrlm  21764  nminvr  24564  deg1pw  26033  ply1nz  26034  mon1pid  26066  ply1remlem  26077  ply1rem  26078  facth1  26079  fta1glem1  26080  fta1glem2  26081  unitnz  33197  drngidl  33411  drngidlhash  33412  prmidl0  33428  drnglidl1ne0  33453  drngmxidlr  33456  krull  33457  qsdrngilem  33472  qsdrngi  33473  qsdrnglem2  33474  qsdrng  33475  ply1moneq  33562  deg1vr  33565  zrhnm  33964  abvexp  42527  uvcn0  42537  0prjspnlem  42618  mon1psubm  43195  nzrneg1ne0  48222  islindeps2  48476