Definition df-csring

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

	Ref	Expression
Assertion	df-csring	$$⊢\mathrm{CSRing}=\left\{f\in \mathrm{SRing}|{\mathrm{mulGrp}}_f\in \mathrm{CMnd}\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccsrg	$$class\mathrm{CSRing}$$
1		vf	$$setvarf$$
2		csrg	$$class\mathrm{SRing}$$
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{SRing}|{\mathrm{mulGrp}}_f\in \mathrm{CMnd}\right\}$$
9	0 8	wceq	$$wff\mathrm{CSRing}=\left\{f\in \mathrm{SRing}|{\mathrm{mulGrp}}_f\in \mathrm{CMnd}\right\}$$