Metamath Proof Explorer

Theorem isrisc

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

Ref Expression
Hypotheses isrisc.1 
|- R e. _V
isrisc.2 
|- S e. _V
Assertion isrisc 
|- ( R ~=R S <-> ( ( R e. RingOps /\ S e. RingOps ) /\ E. f f e. ( R RngIso S ) ) )

Proof

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