Theorem nzrring 20622

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2143   ≠ wne 2958  ‘cfv 6536  0_gc0g 17496  1_rcur 20267  Ringcrg 20319  NzRingcnzr 20618

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-ss 3922  df-nzr 20619

This theorem is used by:  drnglidl1ne0  20625  nzrunit  20631  lringring  20650  rrgnz  20812  domnring  20815  isdomn4  20823  drngidl  21394  prmidl0  21487  domnchr  21691  uvcf1  21951  lindfind2  21977  frlmisfrlm  22007  nminvr  24835  deg1pw  26287  ply1nz  26288  mon1pid  26320  ply1remlem  26331  ply1rem  26332  facth1  26333  fta1glem1  26334  fta1glem2  26335  unitnz  33567  drngidlhash  33750  drngmxidlr  33769  krull  33770  qsdrngilem  33785  qsdrngi  33786  qsdrnglem2  33787  qsdrng  33788  dflring2  33792  ply1moneq  33887  deg1vr  33891  psrnzr  33911  mplnzr  33912  zrhnm  34366  abvexp  43328  uvcn0  43338  0prjspnlem  43383  mon1psubm  43954  nzrneg1ne0  49023  prmrngring  49131  smprngprmrng  49132  islindeps2  49291