Theorem nzrring 20533

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

Syntax hints:   → wi 4   ∈ wcel 2106   ≠ wne 2938  ‘cfv 6563  0_gc0g 17486  1_rcur 20199  Ringcrg 20251  NzRingcnzr 20529

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-ss 3980  df-nzr 20530

This theorem is referenced by:  nzrunit  20541  lringring  20559  rrgnz  20721  domnring  20724  isdomn4  20733  domnchr  21565  uvcf1  21830  lindfind2  21856  frlmisfrlm  21886  nminvr  24706  deg1pw  26175  ply1nz  26176  mon1pid  26208  ply1remlem  26219  ply1rem  26220  facth1  26221  fta1glem1  26222  fta1glem2  26223  unitnz  33229  drngidl  33441  drngidlhash  33442  prmidl0  33458  drnglidl1ne0  33483  drngmxidlr  33486  krull  33487  qsdrngilem  33502  qsdrngi  33503  qsdrnglem2  33504  qsdrng  33505  ply1moneq  33591  deg1vr  33594  zrhnm  33930  abvexp  42519  uvcn0  42529  0prjspnlem  42610  mon1psubm  43188  nzrneg1ne0  48074  islindeps2  48329