Definition df-cring

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

	Ref	Expression
Assertion	df-cring	⊢ CRing = { 𝑓 ∈ Ring ∣ ( mulGrp ‘ 𝑓 ) ∈ CMnd }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccrg	⊢ CRing
1		vf	⊢ 𝑓
2		crg	⊢ Ring
3		cmgp	⊢ mulGrp
4	1	cv	⊢ 𝑓
5	4 3	cfv	⊢ ( mulGrp ‘ 𝑓 )
6		ccmn	⊢ CMnd
7	5 6	wcel	⊢ ( mulGrp ‘ 𝑓 ) ∈ CMnd
8	7 1 2	crab	⊢ { 𝑓 ∈ Ring ∣ ( mulGrp ‘ 𝑓 ) ∈ CMnd }
9	0 8	wceq	⊢ CRing = { 𝑓 ∈ Ring ∣ ( mulGrp ‘ 𝑓 ) ∈ CMnd }