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	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ ( 𝑅 RingOpsIso 𝑆 ) ) → 𝑅 ≃𝑟 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		elex2	⊢ ( 𝐹 ∈ ( 𝑅 RingOpsIso 𝑆 ) → ∃ 𝑓 𝑓 ∈ ( 𝑅 RingOpsIso 𝑆 ) )
2		risc	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) → ( 𝑅 ≃𝑟 𝑆 ↔ ∃ 𝑓 𝑓 ∈ ( 𝑅 RingOpsIso 𝑆 ) ) )
3	1 2	imbitrrid	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) → ( 𝐹 ∈ ( 𝑅 RingOpsIso 𝑆 ) → 𝑅 ≃𝑟 𝑆 ) )
4	3	3impia	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ ( 𝑅 RingOpsIso 𝑆 ) ) → 𝑅 ≃𝑟 𝑆 )