Theorem nzrring 20447

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

Syntax hints:   → wi 4   ∈ wcel 2113   ≠ wne 2930  ‘cfv 6490  0_gc0g 17357  1_rcur 20114  Ringcrg 20166  NzRingcnzr 20443

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-rab 3398  df-ss 3916  df-nzr 20444

This theorem is referenced by:  nzrunit  20455  lringring  20473  rrgnz  20635  domnring  20638  isdomn4  20647  domnchr  21485  uvcf1  21745  lindfind2  21771  frlmisfrlm  21801  nminvr  24611  deg1pw  26080  ply1nz  26081  mon1pid  26113  ply1remlem  26124  ply1rem  26125  facth1  26126  fta1glem1  26127  fta1glem2  26128  unitnz  33270  drngidl  33463  drngidlhash  33464  prmidl0  33480  drnglidl1ne0  33505  drngmxidlr  33508  krull  33509  qsdrngilem  33524  qsdrngi  33525  qsdrnglem2  33526  qsdrng  33527  ply1moneq  33618  deg1vr  33622  zrhnm  34073  abvexp  42729  uvcn0  42739  0prjspnlem  42808  mon1psubm  43383  nzrneg1ne0  48418  islindeps2  48671