Metamath Proof Explorer


Theorem risci

Description: Determine that two rings are isomorphic. (Contributed by Jeff Madsen, 16-Jun-2011)

Ref Expression
Assertion risci
|- ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RngIso S ) ) -> R ~=R S )

Proof

Step Hyp Ref Expression
1 elex2
 |-  ( F e. ( R RngIso S ) -> E. f f e. ( R RngIso S ) )
2 risc
 |-  ( ( R e. RingOps /\ S e. RingOps ) -> ( R ~=R S <-> E. f f e. ( R RngIso S ) ) )
3 1 2 syl5ibr
 |-  ( ( R e. RingOps /\ S e. RingOps ) -> ( F e. ( R RngIso S ) -> R ~=R S ) )
4 3 3impia
 |-  ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RngIso S ) ) -> R ~=R S )