Theorem nzrring 20466

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

Syntax hints:   → wi 4   ∈ wcel 2114   ≠ wne 2933  ‘cfv 6502  0_gc0g 17373  1_rcur 20133  Ringcrg 20185  NzRingcnzr 20462

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-ss 3920  df-nzr 20463

This theorem is referenced by:  nzrunit  20474  lringring  20492  rrgnz  20654  domnring  20657  isdomn4  20666  domnchr  21504  uvcf1  21764  lindfind2  21790  frlmisfrlm  21820  nminvr  24630  deg1pw  26099  ply1nz  26100  mon1pid  26132  ply1remlem  26143  ply1rem  26144  facth1  26145  fta1glem1  26146  fta1glem2  26147  unitnz  33339  drngidl  33532  drngidlhash  33533  prmidl0  33549  drnglidl1ne0  33574  drngmxidlr  33577  krull  33578  qsdrngilem  33593  qsdrngi  33594  qsdrnglem2  33595  qsdrng  33596  ply1moneq  33687  deg1vr  33691  zrhnm  34151  abvexp  42931  uvcn0  42941  0prjspnlem  43010  mon1psubm  43585  nzrneg1ne0  48619  islindeps2  48872