A D1104: Binary relation structure $M = (X \times Y, f)$ is an injective map

(1)	\begin{equation} \forall \, x \in X : \forall \, y, y' \in Y \left( (x, y), (x, y') \in f \quad \implies \quad y = y' \right) \end{equation}	(D358: Right-unique binary relation)
(2)	\begin{equation} \forall \, x \in X : \exists \, y \in Y : (x, y) \in f \end{equation}	(D359: Left-total binary relation)
(3)	\begin{equation} \forall \, x, x' \in X : \forall \, y \in Y \left( (x, y), (x', y) \in f \quad \implies \quad x = x' \right) \end{equation}	(D357: Left-unique binary relation)

A D18: Map $f : X \to Y$ is injective if and only if \begin{equation} \forall \, x, y \in X \left( f(x) = f(y) \quad \implies \quad x = y \right) \end{equation}