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 = { 𝑟 ∈ Ring ∣ ( 1r ‘ 𝑟 ) ≠ ( 0g ‘ 𝑟 ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cnzr	⊢ NzRing
1		vr	⊢ 𝑟
2		crg	⊢ Ring
3		cur	⊢ 1r
4	1	cv	⊢ 𝑟
5	4 3	cfv	⊢ ( 1r ‘ 𝑟 )
6		c0g	⊢ 0g
7	4 6	cfv	⊢ ( 0g ‘ 𝑟 )
8	5 7	wne	⊢ ( 1r ‘ 𝑟 ) ≠ ( 0g ‘ 𝑟 )
9	8 1 2	crab	⊢ { 𝑟 ∈ Ring ∣ ( 1r ‘ 𝑟 ) ≠ ( 0g ‘ 𝑟 ) }
10	0 9	wceq	⊢ NzRing = { 𝑟 ∈ Ring ∣ ( 1r ‘ 𝑟 ) ≠ ( 0g ‘ 𝑟 ) }