| 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 20513 | . . 3 ⊢ NzRing = {𝑟 ∈ Ring ∣ (1r‘𝑟) ≠ (0g‘𝑟)} | |
| 2 | 1 | ssrab3 4082 | . 2 ⊢ NzRing ⊆ Ring |
| 3 | 2 | sseli 3979 | 1 ⊢ (𝑅 ∈ NzRing → 𝑅 ∈ Ring) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∈ wcel 2108 ≠ wne 2940 ‘cfv 6561 0gc0g 17484 1rcur 20178 Ringcrg 20230 NzRingcnzr 20512 |
| 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 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-rab 3437 df-ss 3968 df-nzr 20513 |
| This theorem is referenced by: nzrunit 20524 lringring 20542 rrgnz 20704 domnring 20707 isdomn4 20716 domnchr 21547 uvcf1 21812 lindfind2 21838 frlmisfrlm 21868 nminvr 24690 deg1pw 26160 ply1nz 26161 mon1pid 26193 ply1remlem 26204 ply1rem 26205 facth1 26206 fta1glem1 26207 fta1glem2 26208 unitnz 33243 drngidl 33461 drngidlhash 33462 prmidl0 33478 drnglidl1ne0 33503 drngmxidlr 33506 krull 33507 qsdrngilem 33522 qsdrngi 33523 qsdrnglem2 33524 qsdrng 33525 ply1moneq 33611 deg1vr 33614 zrhnm 33968 abvexp 42542 uvcn0 42552 0prjspnlem 42633 mon1psubm 43211 nzrneg1ne0 48146 islindeps2 48400 |
| Copyright terms: Public domain | W3C validator |