Definition df-crngo

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

	Ref	Expression
Assertion	df-crngo	$$⊢\mathrm{CRingOps}=\mathrm{RingOps}\cap \mathrm{Com2}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccring	$$class\mathrm{CRingOps}$$
1		crngo	$$class\mathrm{RingOps}$$
2		ccm2	$$class\mathrm{Com2}$$
3	1 2	cin	$$class\left(\mathrm{RingOps}\cap \mathrm{Com2}\right)$$
4	0 3	wceq	$$wff\mathrm{CRingOps}=\mathrm{RingOps}\cap \mathrm{Com2}$$