Metamath Proof Explorer

Theorem brrici

Description: Prove isomorphic by an explicit isomorphism. (Contributed by SN, 10-Jan-2025)

Ref Expression
Assertion brrici 
|- ( F e. ( R RingIso S ) -> R ~=r S )

Proof

Step Hyp Ref Expression
1 ne0i 
 |-  ( F e. ( R RingIso S ) -> ( R RingIso S ) =/= (/) )
2 brric 
 |-  ( R ~=r S <-> ( R RingIso S ) =/= (/) )
3 1 2 sylibr 
 |-  ( F e. ( R RingIso S ) -> R ~=r S )