Theorem brrici

Description: Prove isomorphic by an explicit isomorphism. (Contributed by Jeff Madsen, 16-Jun-2011) (Revised by SN, 10-Jan-2025)

	Ref	Expression
Assertion	brrici	$$⊢F\in \left(R\mathrm{RingIso}S\right)\to R{\simeq }_{𝑟}S$$

Proof

Step	Hyp	Ref	Expression
1		ne0i	$$⊢F\in \left(R\mathrm{RingIso}S\right)\to R\mathrm{RingIso}S\ne \varnothing$$
2		brric	$$⊢R{\simeq }_{𝑟}S\leftrightarrow R\mathrm{RingIso}S\ne \varnothing$$
3	1 2	sylibr	$$⊢F\in \left(R\mathrm{RingIso}S\right)\to R{\simeq }_{𝑟}S$$