Metamath Proof Explorer


Theorem risc

Description: The ring isomorphism relation. (Contributed by Jeff Madsen, 16-Jun-2011)

Ref Expression
Assertion risc
|- ( ( R e. RingOps /\ S e. RingOps ) -> ( R ~=R S <-> E. f f e. ( R RngIso S ) ) )

Proof

Step Hyp Ref Expression
1 isriscg
 |-  ( ( R e. RingOps /\ S e. RingOps ) -> ( R ~=R S <-> ( ( R e. RingOps /\ S e. RingOps ) /\ E. f f e. ( R RngIso S ) ) ) )
2 1 bianabs
 |-  ( ( R e. RingOps /\ S e. RingOps ) -> ( R ~=R S <-> E. f f e. ( R RngIso S ) ) )