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