DEF-ID.
The identity relation on $X$ is the binary relation
\[\operatorname{id}_X = \{(x,y)\in X\times X:x=y\}.\]Since $\operatorname{id}_X$ is automatically a function, it can also be called the identity function.
PROP-ID-EMP.
\[\operatorname{id}_\varnothing = \varnothing.\]