Metamath Proof Explorer

Theorem brric

Description: The relation "is isomorphic to" for (unital) rings. (Contributed by AV, 24-Dec-2019)

Ref Expression
Assertion brric 
|- ( R ~=r S <-> ( R RingIso S ) =/= (/) )

Proof

Step Hyp Ref Expression
1 df-ric 
 |-  ~=r = ( `' RingIso " ( _V \ 1o ) )
2 rimfn 
 |-  RingIso Fn ( _V X. _V )
3 1 2 brwitnlem 
 |-  ( R ~=r S <-> ( R RingIso S ) =/= (/) )