Metamath Proof Explorer

Theorem risci

Description: Obsolete theorem, use brrici instead. Determine that two rings are isomorphic. (Contributed by Jeff Madsen, 16-Jun-2011) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	risci	$⊢ (R \in RingOps \land S \in RingOps \land F \in (R RingOpsIso S)) \to R ≃_{𝑟} S$

Proof

Step	Hyp	Ref	Expression
1		elex2	$⊢ F \in (R RingOpsIso S) \to \exists f f \in (R RingOpsIso S)$
2		risc	$⊢ (R \in RingOps \land S \in RingOps) \to (R ≃_{𝑟} S \leftrightarrow \exists f f \in (R RingOpsIso S))$
3	1 2	imbitrrid	$⊢ (R \in RingOps \land S \in RingOps) \to (F \in (R RingOpsIso S) \to R ≃_{𝑟} S)$
4	3	3impia	$⊢ (R \in RingOps \land S \in RingOps \land F \in (R RingOpsIso S)) \to R ≃_{𝑟} S$