Definition df-csring

Description: Define the class of all commutative semirings. (Contributed by metakunt, 4-Apr-2025)

	Ref	Expression
Assertion	df-csring	|- CSRing = { f e. SRing | ( mulGrp ` f ) e. CMnd }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccsrg	|- CSRing
1		vf	|- f
2		csrg	|- SRing
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. SRing | ( mulGrp ` f ) e. CMnd }
9	0 8	wceq	|- CSRing = { f e. SRing | ( mulGrp ` f ) e. CMnd }