Metamath Proof Explorer


Definition df-csring

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

Ref Expression
Assertion df-csring CSRing = f SRing | mulGrp f CMnd

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccsrg class CSRing
1 vf setvar f
2 csrg class SRing
3 cmgp class mulGrp
4 1 cv setvar f
5 4 3 cfv class mulGrp f
6 ccmn class CMnd
7 5 6 wcel wff mulGrp f CMnd
8 7 1 2 crab class f SRing | mulGrp f CMnd
9 0 8 wceq wff CSRing = f SRing | mulGrp f CMnd