Metamath Proof Explorer


Theorem risci

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

Ref Expression
Assertion risci R RingOps S RingOps F R RngIso S R 𝑟 S

Proof

Step Hyp Ref Expression
1 elex2 F R RngIso S f f R RngIso S
2 risc R RingOps S RingOps R 𝑟 S f f R RngIso S
3 1 2 syl5ibr R RingOps S RingOps F R RngIso S R 𝑟 S
4 3 3impia R RingOps S RingOps F R RngIso S R 𝑟 S