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	⊢ ( 𝑥 = 𝑦 → 𝑥 = 𝑦 )
2		df-id	⊢ I = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 = 𝑦 }
3	1 2	eqer	⊢ I Er V