Identity

DEF-ID.

The identity on $X$ is the binary relation

\[\id_X = \{(x,x):x\in X\}.\]

PROP-ID-F.

For any $X$, $\id_X$ is also a function.

PROP-ID-EMP.

\[\id_\varnothing = \varnothing.\]