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 e. Ring | ( 1r ` r ) =/= ( 0g ` r ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cnzr	|- NzRing
1		vr	|- r
2		crg	|- Ring
3		cur	|- 1r
4	1	cv	|- r
5	4 3	cfv	|- ( 1r ` r )
6		c0g	|- 0g
7	4 6	cfv	|- ( 0g ` r )
8	5 7	wne	|- ( 1r ` r ) =/= ( 0g ` r )
9	8 1 2	crab	|- { r e. Ring | ( 1r ` r ) =/= ( 0g ` r ) }
10	0 9	wceq	|- NzRing = { r e. Ring | ( 1r ` r ) =/= ( 0g ` r ) }