Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Jeff Madsen
Commutative rings
df-crngo
Next ⟩
iscom2
Metamath Proof Explorer
Ascii
Unicode
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