Theorem ider

Description: The identity relation is an equivalence relation. (Contributed by NM, 10-May-1998) (Proof shortened by Andrew Salmon, 22-Oct-2011) (Proof shortened by Mario Carneiro, 9-Jul-2014)

	Ref	Expression
Assertion	ider	|- _I Er _V

Proof

Step	Hyp	Ref	Expression
1		id	|- ( x = y -> x = y )
2		df-id	|- _I = { <. x , y >. | x = y }
3	1 2	eqer	|- _I Er _V