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	⊢ ≃𝑟 Er Ring

Proof

Step	Hyp	Ref	Expression
1		ricrel	⊢ Rel ≃𝑟
2		ricsym	⊢ ( 𝑥 ≃𝑟 𝑦 → 𝑦 ≃𝑟 𝑥 )
3		rictr	⊢ ( ( 𝑥 ≃𝑟 𝑦 ∧ 𝑦 ≃𝑟 𝑧 ) → 𝑥 ≃𝑟 𝑧 )
4		ricref	⊢ ( 𝑥 ∈ Ring → 𝑥 ≃𝑟 𝑥 )
5		riclcl	⊢ ( 𝑥 ≃𝑟 𝑥 → 𝑥 ∈ Ring )
6	4 5	impbii	⊢ ( 𝑥 ∈ Ring ↔ 𝑥 ≃𝑟 𝑥 )
7	1 2 3 6	iseri	⊢ ≃𝑟 Er Ring