Description: The relation "is isomorphic to" for (unital) rings. This theorem corresponds to the definition df-risc of the ring isomorphism relation in JM's mathbox. (Contributed by AV, 24-Dec-2019)