Metamath Proof Explorer

Theorem risc

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

		Ref	Expression
	Assertion	risc	$⊢ (R \in RingOps \land S \in RingOps) \to (R ≃_{𝑟} S \leftrightarrow \exists f f \in (R RngIso S))$

Step	Hyp	Ref	Expression
1		isriscg	$⊢ (R \in RingOps \land S \in RingOps) \to (R ≃_{𝑟} S \leftrightarrow ((R \in RingOps \land S \in RingOps) \land \exists f f \in (R RngIso S)))$
2	1	bianabs	$⊢ (R \in RingOps \land S \in RingOps) \to (R ≃_{𝑟} S \leftrightarrow \exists f f \in (R RngIso S))$