This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ NzRing = \{r \in Ring \| 1_{r} \neq 0_{r}\}$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cnzr	$class NzRing$
1		vr	$setvar r$
2		crg	$class Ring$
3		cur	$class 1_{r}$
4	1	cv	$setvar r$
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} \neq 0_{r}$
9	8 1 2	crab	$class \{r \in Ring \| 1_{r} \neq 0_{r}\}$
10	0 9	wceq	$wff NzRing = \{r \in Ring \| 1_{r} \neq 0_{r}\}$