Theorem nzrring 20516

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

Syntax hints:   → wi 4   ∈ wcel 2108   ≠ wne 2940  ‘cfv 6561  0_gc0g 17484  1_rcur 20178  Ringcrg 20230  NzRingcnzr 20512

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-ss 3968  df-nzr 20513

This theorem is referenced by:  nzrunit  20524  lringring  20542  rrgnz  20704  domnring  20707  isdomn4  20716  domnchr  21547  uvcf1  21812  lindfind2  21838  frlmisfrlm  21868  nminvr  24690  deg1pw  26160  ply1nz  26161  mon1pid  26193  ply1remlem  26204  ply1rem  26205  facth1  26206  fta1glem1  26207  fta1glem2  26208  unitnz  33243  drngidl  33461  drngidlhash  33462  prmidl0  33478  drnglidl1ne0  33503  drngmxidlr  33506  krull  33507  qsdrngilem  33522  qsdrngi  33523  qsdrnglem2  33524  qsdrng  33525  ply1moneq  33611  deg1vr  33614  zrhnm  33968  abvexp  42542  uvcn0  42552  0prjspnlem  42633  mon1psubm  43211  nzrneg1ne0  48146  islindeps2  48400