Theorem nzrring 20407

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

Syntax hints:   → wi 4   ∈ wcel 2104   ≠ wne 2938  ‘cfv 6542  0_gc0g 17389  1_rcur 20075  Ringcrg 20127  NzRingcnzr 20403

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-rab 3431  df-v 3474  df-in 3954  df-ss 3964  df-nzr 20404

This theorem is referenced by:  opprnzr  20411  nzrunit  20413  lringring  20430  domnring  21112  isdomn4  21118  domnchr  21303  uvcf1  21566  lindfind2  21592  frlmisfrlm  21622  nminvr  24406  deg1pw  25873  ply1nz  25874  ply1remlem  25915  ply1rem  25916  facth1  25917  fta1glem1  25918  fta1glem2  25919  drngidl  32825  drngidlhash  32826  prmidl0  32843  drnglidl1ne0  32865  krull  32868  qsdrngilem  32882  qsdrngi  32883  qsdrnglem2  32884  qsdrng  32885  ply1moneq  32939  zrhnm  33247  uvcn0  41414  0prjspnlem  41667  mon1pid  42249  mon1psubm  42250  nzrneg1ne0  46909  islindeps2  47251