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 ) )