Definition df-cring

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

	Ref	Expression
Assertion	df-cring	|- CRing = { f e. Ring | ( mulGrp ` f ) e. CMnd }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccrg	|- CRing
1		vf	|- f
2		crg	|- Ring
3		cmgp	|- mulGrp
4	1	cv	|- f
5	4 3	cfv	|- ( mulGrp ` f )
6		ccmn	|- CMnd
7	5 6	wcel	|- ( mulGrp ` f ) e. CMnd
8	7 1 2	crab	|- { f e. Ring | ( mulGrp ` f ) e. CMnd }
9	0 8	wceq	|- CRing = { f e. Ring | ( mulGrp ` f ) e. CMnd }