Metamath Proof Explorer


Definition df-crngo

Description: Define the class of commutative rings. (Contributed by Jeff Madsen, 8-Jun-2010)

Ref Expression
Assertion df-crngo CRingOps = RingOps Com2

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccring class CRingOps
1 crngo class RingOps
2 ccm2 class Com2
3 1 2 cin class RingOps Com2
4 0 3 wceq wff CRingOps = RingOps Com2