Theorem brric

Description: The relation "is isomorphic to" for (unital) rings. (Contributed by AV, 24-Dec-2019)

	Ref	Expression
Assertion	brric	$$⊢R{\simeq }_{𝑟}S\leftrightarrow R\mathrm{RingIso}S\ne \varnothing$$

Proof

Step	Hyp	Ref	Expression
1		df-ric	$$⊢{\simeq }_{𝑟}={\mathrm{RingIso}}^{-1}\left[\mathrm{V}\setminus 1_{𝑜}\right]$$
2		rimfn	$$⊢\mathrm{RingIso}Fn\left(\mathrm{V}\times \mathrm{V}\right)$$
3	1 2	brwitnlem	$$⊢R{\simeq }_{𝑟}S\leftrightarrow R\mathrm{RingIso}S\ne \varnothing$$