Theorem ricer

Description: Ring isomorphism is an equivalence relation. (Contributed by Jeff Madsen, 16-Jun-2011) (Revised by Mario Carneiro, 12-Aug-2015) (Revised by AV, 24-Jul-2026)

	Ref	Expression
Assertion	ricer	$$⊢{\simeq }_{𝑟}\mathrm{Er}\mathrm{Ring}$$

Proof

Step	Hyp	Ref	Expression
1		ricrel	$$⊢\mathrm{Rel}{\simeq }_{𝑟}$$
2		ricsym	$$⊢x{\simeq }_{𝑟}y\to y{\simeq }_{𝑟}x$$
3		rictr	$$⊢\left(x{\simeq }_{𝑟}y\wedge y{\simeq }_{𝑟}z\right)\to x{\simeq }_{𝑟}z$$
4		ricref	$$⊢x\in \mathrm{Ring}\to x{\simeq }_{𝑟}x$$
5		riclcl	$$⊢x{\simeq }_{𝑟}x\to x\in \mathrm{Ring}$$
6	4 5	impbii	$$⊢x\in \mathrm{Ring}\leftrightarrow x{\simeq }_{𝑟}x$$
7	1 2 3 6	iseri	$$⊢{\simeq }_{𝑟}\mathrm{Er}\mathrm{Ring}$$