Metamath Proof Explorer

Theorem iscrngo

Description: The predicate "is a commutative ring". (Contributed by Jeff Madsen, 8-Jun-2010)

Ref Expression
Assertion iscrngo 
|- ( R e. CRingOps <-> ( R e. RingOps /\ R e. Com2 ) )

Proof

Step Hyp Ref Expression
1 df-crngo 
 |-  CRingOps = ( RingOps i^i Com2 )
2 1 elin2 
 |-  ( R e. CRingOps <-> ( R e. RingOps /\ R e. Com2 ) )