![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nzrring | Structured version Visualization version GIF version |
Description: A nonzero ring is a ring. (Contributed by Stefan O'Rear, 24-Feb-2015.) (Proof shortened by SN, 23-Feb-2025.) |
Ref | Expression |
---|---|
nzrring | ⊢ (𝑅 ∈ NzRing → 𝑅 ∈ Ring) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-nzr 20495 | . . 3 ⊢ NzRing = {𝑟 ∈ Ring ∣ (1r‘𝑟) ≠ (0g‘𝑟)} | |
2 | 1 | ssrab3 4079 | . 2 ⊢ NzRing ⊆ Ring |
3 | 2 | sseli 3975 | 1 ⊢ (𝑅 ∈ NzRing → 𝑅 ∈ Ring) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2099 ≠ wne 2930 ‘cfv 6554 0gc0g 17454 1rcur 20164 Ringcrg 20216 NzRingcnzr 20494 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-rab 3420 df-ss 3964 df-nzr 20495 |
This theorem is referenced by: nzrunit 20506 lringring 20524 rrgnz 20682 domnring 20685 isdomn4 20694 domnchr 21526 uvcf1 21790 lindfind2 21816 frlmisfrlm 21846 nminvr 24677 deg1pw 26148 ply1nz 26149 mon1pid 26181 ply1remlem 26192 ply1rem 26193 facth1 26194 fta1glem1 26195 fta1glem2 26196 unitnz 33104 drngidl 33308 drngidlhash 33309 prmidl0 33325 drnglidl1ne0 33350 drngmxidlr 33353 krull 33354 qsdrngilem 33369 qsdrngi 33370 qsdrnglem2 33371 qsdrng 33372 ply1moneq 33458 deg1vr 33461 zrhnm 33784 uvcn0 42014 0prjspnlem 42277 mon1psubm 42864 nzrneg1ne0 47607 islindeps2 47866 |
Copyright terms: Public domain | W3C validator |