Identity relation
Set
$X$
$ \langle x,y\rangle \in\text{id}_X $
$ \langle x,y\rangle \in \text{unaryOp}(X) $
$ x=y $
Ramifications
Reference
Mizar files:
RELAT_1
Wikipedia:
Equality
Parents
Subset of
Unary operation