Definition df-crngo

Description: Define the class of commutative rings. (Contributed by Jeff Madsen, 8-Jun-2010)

	Ref	Expression
Assertion	df-crngo	⊢ CRingOps = ( RingOps ∩ Com2 )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccring	⊢ CRingOps
1		crngo	⊢ RingOps
2		ccm2	⊢ Com2
3	1 2	cin	⊢ ( RingOps ∩ Com2 )
4	0 3	wceq	⊢ CRingOps = ( RingOps ∩ Com2 )