Metamath Proof Explorer

Theorem brric2

Description: The ring isomorphism relation. (Contributed by Jeff Madsen, 16-Jun-2011) (Revised by AV, 23-Jul-2026)

		Ref	Expression
	Assertion	brric2	$⊢ (R \in Ring \land S \in Ring) \to (R ≃_{𝑟} S \leftrightarrow \exists f f \in (R RingIso S))$

Step	Hyp	Ref	Expression
1		isbrric2	$⊢ R ≃_{𝑟} S \leftrightarrow ((R \in Ring \land S \in Ring) \land \exists f f \in (R RingIso S))$
2	1	baib	$⊢ (R \in Ring \land S \in Ring) \to (R ≃_{𝑟} S \leftrightarrow \exists f f \in (R RingIso S))$