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 i^i Com2 )

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccring 
 |-  CRingOps
1 crngo 
 |-  RingOps
2 ccm2 
 |-  Com2
3 1 2 cin 
 |-  ( RingOps i^i Com2 )
4 0 3 wceq 
 |-  CRingOps = ( RingOps i^i Com2 )