Theorem nzrring 20568

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

Syntax hints:   → wi 4   ∈ wcel 2144   ≠ wne 2959  ‘cfv 6523  0_gc0g 17470  1_rcur 20233  Ringcrg 20285  NzRingcnzr 20564

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-rab 3417  df-ss 3923  df-nzr 20565

This theorem is referenced by:  nzrunit  20576  lringring  20594  rrgnz  20756  domnring  20759  isdomn4  20768  domnchr  21586  uvcf1  21846  lindfind2  21872  frlmisfrlm  21902  nminvr  24731  deg1pw  26183  ply1nz  26184  mon1pid  26216  ply1remlem  26227  ply1rem  26228  facth1  26229  fta1glem1  26230  fta1glem2  26231  unitnz  33421  drngidl  33621  drngidlhash  33622  prmidl0  33639  drnglidl1ne0  33665  drngmxidlr  33668  krull  33669  qsdrngilem  33684  qsdrngi  33685  qsdrnglem2  33686  qsdrng  33687  dflring2  33691  ply1moneq  33786  deg1vr  33790  psrnzr  33811  mplnzr  33812  zrhnm  34266  abvexp  43155  uvcn0  43165  0prjspnlem  43210  mon1psubm  43781  nzrneg1ne0  48857  islindeps2  49110