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	$$⊢\mathrm{I}\mathrm{Er}\mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		id	$$⊢x=y\to x=y$$
2		df-id	$$⊢\mathrm{I}=\left\{⟨x,y⟩|x=y\right\}$$
3	1 2	eqer	$$⊢\mathrm{I}\mathrm{Er}\mathrm{V}$$