Metamath Proof Explorer

Theorem brric2

Description: The ring isomorphism relation. (Contributed by Jeff Madsen, 16-Jun-2011) (Revised by AV, 23-Jul-2026)

Ref Expression
Assertion brric2 
|- ( ( R e. Ring /\ S e. Ring ) -> ( R ~=r S <-> E. f f e. ( R RingIso S ) ) )

Proof

Step Hyp Ref Expression
1 isbrric2 
 |-  ( R ~=r S <-> ( ( R e. Ring /\ S e. Ring ) /\ E. f f e. ( R RingIso S ) ) )
2 1 baib 
 |-  ( ( R e. Ring /\ S e. Ring ) -> ( R ~=r S <-> E. f f e. ( R RingIso S ) ) )