Theorem nzrring 20476

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

Syntax hints:   → wi 4   ∈ wcel 2108   ≠ wne 2932  ‘cfv 6531  0_gc0g 17453  1_rcur 20141  Ringcrg 20193  NzRingcnzr 20472

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 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-ss 3943  df-nzr 20473

This theorem is referenced by:  nzrunit  20484  lringring  20502  rrgnz  20664  domnring  20667  isdomn4  20676  domnchr  21493  uvcf1  21752  lindfind2  21778  frlmisfrlm  21808  nminvr  24608  deg1pw  26078  ply1nz  26079  mon1pid  26111  ply1remlem  26122  ply1rem  26123  facth1  26124  fta1glem1  26125  fta1glem2  26126  unitnz  33234  drngidl  33448  drngidlhash  33449  prmidl0  33465  drnglidl1ne0  33490  drngmxidlr  33493  krull  33494  qsdrngilem  33509  qsdrngi  33510  qsdrnglem2  33511  qsdrng  33512  ply1moneq  33599  deg1vr  33602  zrhnm  33998  abvexp  42555  uvcn0  42565  0prjspnlem  42646  mon1psubm  43223  nzrneg1ne0  48205  islindeps2  48459