Definition df-cring

Description: Define class of all commutative rings. (Contributed by Mario Carneiro, 7-Jan-2015)

	Ref	Expression
Assertion	df-cring	$$⊢\mathrm{CRing}=\left\{f\in \mathrm{Ring}|{\mathrm{mulGrp}}_f\in \mathrm{CMnd}\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccrg	$$class\mathrm{CRing}$$
1		vf	$$setvarf$$
2		crg	$$class\mathrm{Ring}$$
3		cmgp	$$class\mathrm{mulGrp}$$
4	1	cv	$$setvarf$$
5	4 3	cfv	$$class{\mathrm{mulGrp}}_f$$
6		ccmn	$$class\mathrm{CMnd}$$
7	5 6	wcel	$$wff{\mathrm{mulGrp}}_f\in \mathrm{CMnd}$$
8	7 1 2	crab	$$class\left\{f\in \mathrm{Ring}|{\mathrm{mulGrp}}_f\in \mathrm{CMnd}\right\}$$
9	0 8	wceq	$$wff\mathrm{CRing}=\left\{f\in \mathrm{Ring}|{\mathrm{mulGrp}}_f\in \mathrm{CMnd}\right\}$$