Theorem nzrring 20425

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

Syntax hints:   → wi 4   ∈ wcel 2109   ≠ wne 2925  ‘cfv 6511  0_gc0g 17402  1_rcur 20090  Ringcrg 20142  NzRingcnzr 20421

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 3406  df-ss 3931  df-nzr 20422

This theorem is referenced by:  nzrunit  20433  lringring  20451  rrgnz  20613  domnring  20616  isdomn4  20625  domnchr  21442  uvcf1  21701  lindfind2  21727  frlmisfrlm  21757  nminvr  24557  deg1pw  26026  ply1nz  26027  mon1pid  26059  ply1remlem  26070  ply1rem  26071  facth1  26072  fta1glem1  26073  fta1glem2  26074  unitnz  33190  drngidl  33404  drngidlhash  33405  prmidl0  33421  drnglidl1ne0  33446  drngmxidlr  33449  krull  33450  qsdrngilem  33465  qsdrngi  33466  qsdrnglem2  33467  qsdrng  33468  ply1moneq  33555  deg1vr  33558  zrhnm  33957  abvexp  42520  uvcn0  42530  0prjspnlem  42611  mon1psubm  43188  nzrneg1ne0  48218  islindeps2  48472