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	|- ~=r Er Ring

Proof

Step	Hyp	Ref	Expression
1		ricrel	|- Rel ~=r
2		ricsym	|- ( x ~=r y -> y ~=r x )
3		rictr	|- ( ( x ~=r y /\ y ~=r z ) -> x ~=r z )
4		ricref	|- ( x e. Ring -> x ~=r x )
5		riclcl	|- ( x ~=r x -> x e. Ring )
6	4 5	impbii	|- ( x e. Ring <-> x ~=r x )
7	1 2 3 6	iseri	|- ~=r Er Ring