Metamath Proof Explorer


Theorem risc

Description: The ring isomorphism relation. (Contributed by Jeff Madsen, 16-Jun-2011)

Ref Expression
Assertion risc ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) → ( 𝑅𝑟 𝑆 ↔ ∃ 𝑓 𝑓 ∈ ( 𝑅 RngIso 𝑆 ) ) )

Proof

Step Hyp Ref Expression
1 isriscg ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) → ( 𝑅𝑟 𝑆 ↔ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) ∧ ∃ 𝑓 𝑓 ∈ ( 𝑅 RngIso 𝑆 ) ) ) )
2 1 bianabs ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) → ( 𝑅𝑟 𝑆 ↔ ∃ 𝑓 𝑓 ∈ ( 𝑅 RngIso 𝑆 ) ) )