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 ) |
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 ) |