Definition df-nzr

Description: A nonzero or nontrivial ring is a ring with at least two values, or equivalently where 1 and 0 are different. (Contributed by Stefan O'Rear, 24-Feb-2015)

	Ref	Expression
Assertion	df-nzr	$$⊢\mathrm{NzRing}=\left\{r\in \mathrm{Ring}|1_r\ne 0_r\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cnzr	$$class\mathrm{NzRing}$$
1		vr	$$setvarr$$
2		crg	$$class\mathrm{Ring}$$
3		cur	$$class{1}_r$$
4	1	cv	$$setvarr$$
5	4 3	cfv	$$class{1}_r$$
6		c0g	$$class{0}_{𝑔}$$
7	4 6	cfv	$$class{0}_r$$
8	5 7	wne	$$wff{1}_r\ne 0_r$$
9	8 1 2	crab	$$class\left\{r\in \mathrm{Ring}|1_r\ne 0_r\right\}$$
10	0 9	wceq	$$wff\mathrm{NzRing}=\left\{r\in \mathrm{Ring}|1_r\ne 0_r\right\}$$