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\in \mathrm{NzRing}\to R\in \mathrm{Ring}$$

Proof

Step	Hyp	Ref	Expression
1		df-nzr	$$⊢\mathrm{NzRing}=\left\{r\in \mathrm{Ring}|1_r\ne 0_r\right\}$$
2	1	ssrab3	$$⊢\mathrm{NzRing}\subseteq \mathrm{Ring}$$
3	2	sseli	$$⊢R\in \mathrm{NzRing}\to R\in \mathrm{Ring}$$