Metamath Proof Explorer

Theorem nzrring

Description: A nonzero ring is a ring. (Contributed by Stefan O'Rear, 24-Feb-2015) (Proof shortened by SN, 23-Feb-2025)

Ref Expression
Assertion nzrring 
|- ( R e. NzRing -> R e. Ring )

Proof

Step Hyp Ref Expression
1 df-nzr 
 |-  NzRing = { r e. Ring | ( 1r ` r ) =/= ( 0g ` r ) }
2 1 ssrab3 
 |-  NzRing C_ Ring
3 2 sseli 
 |-  ( R e. NzRing -> R e. Ring )