Metamath Proof Explorer


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