Theorem nzrring 20436

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

Syntax hints:   → wi 4   ∈ wcel 2109   ≠ wne 2925  ‘cfv 6499  0_gc0g 17378  1_rcur 20101  Ringcrg 20153  NzRingcnzr 20432

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-ss 3928  df-nzr 20433

This theorem is referenced by:  nzrunit  20444  lringring  20462  rrgnz  20624  domnring  20627  isdomn4  20636  domnchr  21474  uvcf1  21734  lindfind2  21760  frlmisfrlm  21790  nminvr  24590  deg1pw  26059  ply1nz  26060  mon1pid  26092  ply1remlem  26103  ply1rem  26104  facth1  26105  fta1glem1  26106  fta1glem2  26107  unitnz  33206  drngidl  33397  drngidlhash  33398  prmidl0  33414  drnglidl1ne0  33439  drngmxidlr  33442  krull  33443  qsdrngilem  33458  qsdrngi  33459  qsdrnglem2  33460  qsdrng  33461  ply1moneq  33548  deg1vr  33551  zrhnm  33950  abvexp  42513  uvcn0  42523  0prjspnlem  42604  mon1psubm  43181  nzrneg1ne0  48211  islindeps2  48465